archives

Preliminary Design of JML: A Behavioral Interface Specification


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Leavens, Gary, Baker, Albert and Ruby, Clyde (1998) Preliminary Design of JML: A Behavioral Interface Specification. Technical Report TR98-06b, Department of Computer Science, Iowa State University.

Full text available as:Postscript
Adobe PDF

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, and requires only modest mathematical training.
To achieve this goal, 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 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:00000196
Deposited by:Staff Account on 04 November 1998



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