Preliminary Design of JML: A Behavioral Interface Specification Language for Java

Leavens, Gary T., Baker, Albert L. and Ruby, Clyde (1999) Preliminary Design of JML: A Behavioral Interface Specification Language for Java. Technical Report TR98-06f, Department of Computer Science, Iowa State University.

Abstract

Preliminary Design of JML:
A Behavioral Interface Specification Language for Java
by
Gary T. Leavens, Albert L. Baker, and Clyde Ruby
Abstract
JML is a behavioral interface specification language tailored to Java.
It also allows assertions to be intermixed with Java code, as an aid
to verification and debugging.  JML is designed to be used by working
software engineers.  To achieve these goals, JML uses Eiffel-style
assertion syntax combined with the model-based approach to
specifications typified by VDM and Larch.  However, JML supports
quantifiers, specification-only variables, frame conditions, and other
enhancements that make it more expressive for specification than
Eiffel.
This paper discusses the goals of JML, the overall approach, and
describes the basic features of the language through examples.  It is
intended for readers who have some familiarity with both Java and
behavioral specification using pre- and postconditions.
Keywords: Behavioral interface specification, Java,
JML, Eiffel, Larch, model-based specification,
precondition, postcondition, frame.
1997 CR Categories:
D.2.1 [Software Engineering]
Requirements/Specifications -- languages, theory, Larch, Eiffel, JML;
D.2.7 [Software Engineering]
Distribution and Maintenance --- documentation;
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs --
assertions, logics of programs, pre- and post-conditions,
specification techniques.


Subjects:
All uncategorized technical reports


ID code:
00000203
Deposited by:
Staff Account on 06 July 1999





Contact site administrator at: ssg@cs.iastate.edu