archives

Desugaring JML Method Specifications


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Raghavan, Arun D. and Leavens, Gary T. (2000) Desugaring JML Method Specifications. Technical Report TR00-03a, Department of Computer Science, Iowa State University.

Full text available as:Postscript

Abstract

Desugaring JML Method Specifications
by
Arun D. Raghavan and Gary T. Leavens
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
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.
1999 CR Categories:
D.2.4 [Software Engineering] Software/Program Verification
--- Formal methods, programming by contract, reliability, tools,
JML;
D.2.7 [Software Engineering] Distribution, Maintenance, and Enhancement
--- Documentation;
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs ---
Assertions, pre- and post-conditions,
specification techniques;
Copyright (c) 2000 by Arun D. Raghavan and Gary T. Leavens.

Subjects:All uncategorized technical reports
ID code:00000222
Deposited by:Staff Account on 13 July 2000



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