BOB ATKEY

Specifying and Verifying Heap Space Allocation with JML and ESC/Java2

Publication Information

Robert Atkey. Specifying and Verifying Heap Space Allocation with JML and ESC/Java2. In 8th Workshop for Formal Techniques for Java-like Programs (FtfJP2006). 2006.

Abstract

We examine JML’s support for specifying the heap space allocation of Java programs. In this report we restrict ourselves to specifying and verifying only allocation but not de-allocation. We identify some problems with with JML’s support and suggest alternatives. Also, we describe an implementation of heap space allocation verification in ESC/Java2. This implementation has been tested on small examples.