Raghavan, Arun D. and Leavens, Gary T. (2000) Desugaring JML Method Specifications. Technical Report TR00-03, Department of Computer Science, Iowa State University.
Desugaring JML Method Specifications
Arun D. Raghavan and Gary T. Leavens
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 specifications more expressive. This paper presents
a desugaring process that boils down all of the syntactic sugars in
JML into a much simpler form. This desugaring will help one
manipulate JML specifications in tools, understand the meaning of
these sugars, and it also allows the use of JML specifications in
Keywords: Behavioral interface specification language,
formal specification, desugaring, semantics
model-based specification, formal methods,
precondition, postcondition, JML.
1999 CR Categories:
D.2.4 [Software Engineering] Software/Program Verification
--- Formal methods, programming by contract, reliability, tools,
D.2.7 [Software Engineering] Distribution, Maintenance, and Enhancement
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs ---
Assertions, pre- and post-conditions,
Copyright (c) 2000 by Arun D. Raghavan and Gary T. Leavens.
Contact site administrator at: firstname.lastname@example.org