archives

Desugaring JML Method Specifications


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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

Full text available as:Adobe PDF
Postscript

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 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 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:00000248
Deposited by:Gary T. Leavens on 27 August 2001
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/TR.ps.gz ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/TR.pdf



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