Desugaring JML Method Specifications
|
Home About Browse Search Register Subscriptions Deposit Papers Help |
Leavens, Gary T. and Raghavan, Arun (2003) Desugaring JML Method Specifications. Technical Report 00-03d, 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, 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 manipulate JML method specifications in tools, understand the meaning of these sugars, and it also allows the use of JML method specifications in program verification.
| 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) 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: | 00000306 |
| Deposited by: | Gary T. Leavens |
| Alternative Locations: | ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/TR.ps.gz |
Available Versions of This Paper
- Desugaring JML Method Specifications (deposited 07 July 2003) [Currently displayed]
Contact site administrator at: ssg@cs.iastate.edu