Desugaring JML Method Specifications
Arun D. Raghavan, Gary T. Leavens · 2005
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. 1 Introduction JML [5], which stands for "Java Modeling Language," is a behavioral interface specification language (BISL) [7] designed to specify Java [1, 3] modules. JML features a great deal of syntactic sugar that is designed to make specifications more expressive [4]. Syntactic sugars are additions to a language that make it easier for humans to use. Syntactic sugar gives the user an easier to use notation that can be easily translated, i.e., desuga...