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

Robert Atkey

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

Robert Atkey

Computer And Information Sciences

Research output: Contribution to conference › Paper › peer-review

15 Downloads (Pure)

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 veriﬁcation in ESC/Java2. This implementation has been tested on small examples.

Original language	English
Publication status	Published - 2006
Event	Formal Techniques for Java-like Programs - Nantes, France Duration: 4 Jul 2006 → 4 Jul 2006

Conference

Conference	Formal Techniques for Java-like Programs
Abbreviated title	FTfJP
Country/Territory	France
City	Nantes
Period	4/07/06 → 4/07/06

Keywords

heap space allocation
Java2
Java Modelling Language
Java classes

Access to Document

Atkey-FTJP-2006-Specifying-and-verifying-heap-space-allocation-with-JML-and-ESC-Java2Accepted author manuscript, 170 KB

Cite this

@conference{651c0dee6f3044309a64f5f227a15eef,

title = "Specifying and verifying heap space allocation with JML and ESC/Java2",

abstract = "We examine JML{\textquoteright}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{\textquoteright}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.",

keywords = "heap space allocation, Java2, Java Modelling Language, Java classes",

author = "Robert Atkey",

year = "2006",

language = "English",

note = "Formal Techniques for Java-like Programs, FTfJP ; Conference date: 04-07-2006 Through 04-07-2006",

}

TY - CONF

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

AU - Atkey, Robert

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

KW - heap space allocation

KW - Java2

KW - Java Modelling Language

KW - Java classes

M3 - Paper

T2 - Formal Techniques for Java-like Programs

Y2 - 4 July 2006 through 4 July 2006

ER -

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

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this