Desugaring JML Method Specifications







Deposit Papers 


Raghavan, Arun D. and Leavens, Gary T. (2005) Desugaring JML Method Specifications. Technical Report 00-03e, Computer Science, Iowa State University.

Full text available as:Adobe PDF

This is the latest version of this eprint.


JML, which stands for ``Java Modeling Language,'' is a behavioral interface specification language (BISL) designed to specify Java modules. JML features a great deal of syntactic sugar that is designed to make method specifications more expressive. This paper presents a desugaring process that boils down all of the syntactic sugars in JML method specifications into a much simpler form. This desugaring will help one understand the meaning of these sugars, for example for use in program verification. It may also help manipulation of JML method specifications by tools.

Keywords:Behavioral interface specification language, formal specification, desugaring, semantics, specification inheritance, refinement, behavioral subtyping, model-based specification, formal methods, precondition, postcondition, Eiffel, Java, 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:00000372
Deposited by:Gary T. Leavens on 03 June 2005
Alternative Locations:

Available Versions of This Paper

Contact site administrator at: