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







Deposit Papers 


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

Full text available as:Postscript


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 do this it follows Eiffel in using Java expressions in assertions. JML combines this idea from Eiffel with the model-based approach to specifications, typified by VDM and Larch, which results in greater expressiveness. Other expressiveness advantages over Eiffel include quantifiers, specification-only variables, and frame conditions. This paper discusses the goals of JML, the overall pproach, 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, assertion, precondition, postcondition, frame
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Distribution, Maintenance, and Enhancement
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
ID code:00000235
Deposited by:Staff Account on 13 March 2001

Commentary/Response Threads

Contact site administrator at: