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

Research output: Contribution to conferencePaper

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.
Original languageEnglish
Publication statusPublished - 2006
EventFormal Techniques for Java-like Programs - Nantes, France
Duration: 4 Jul 20064 Jul 2006

Conference

ConferenceFormal Techniques for Java-like Programs
Abbreviated titleFTfJP
CountryFrance
CityNantes
Period4/07/064/07/06

Keywords

  • heap space allocation
  • Java2
  • Java Modelling Language
  • Java classes

Cite this