archives

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


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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

Full text available as:Adobe PDF
Postscript

There is a later version of this eprint available: Click here to view it.

Abstract

JML is a behavioral interface specification language tailored to Java(TM). Besides pre- and postconditions, it also allows assertions to be intermixed with Java code; these aid 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 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, assertion, precondition, postcondition, frame.
Comments:See www.jmlspecs.org for more about JML
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
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)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
ID code:00000355
Deposited by:Gary T. Leavens on 24 February 2005
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/leavens/JML/prelimdesign.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz

Available Versions of This Paper



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