Specifying and Verifying Heap Space Allocation with JML and ESC/Java2
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.
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 veriﬁcation in ESC/Java2. This implementation has been tested on small examples.