Publication Date

5-2005

Technical Report Number

TR00-03e

Subjects

Software, Theory of Computation

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 understand the meaning of these sugars, for example for use in program verification. It may also help manipulation of JML method specifications by tools.

Comments

Copyright © 2000, 2001, 2003, 2005 by Iowa State University

Share

COinS