Specifying and verifying heap space allocation with JML and ESC/Java2

Atkey, Robert (2006) Specifying and verifying heap space allocation with JML and ESC/Java2. In: Formal Techniques for Java-like Programs, 2006-07-04 - 2006-07-04.

[thumbnail of Atkey-FTJP-2006-Specifying-and-verifying-heap-space-allocation-with-JML-and-ESC-Java2]
Preview
Text. Filename: Atkey_FTJP_2006_Specifying_and_verifying_heap_space_allocation_with_JML_and_ESC_Java2.pdf
Accepted Author Manuscript

Download (174kB)| Preview

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.