Leavens, Gary T., Baker, Albert L. and Ruby, Clyde (1998) Preliminary Design of JML: A Behavioral Interface Specification Language for Java. Technical Report TR98-06, Department of Computer Science, Iowa State University.
Preliminary Design of JML:
A Behavioral Interface Specification Language for Java
Gary T. Leavens, Albert L. Baker, and Clyde Ruby
JML is a behavioral interface specification language tailored to Java.
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 model-based approach to
specifications. 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,
- Leavens, Gary T., Baker, Albert L. and Ruby, Clyde. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. (deposited 05 June 1998) [Currently displayed]
Contact site administrator at: email@example.com