Technical Report Number
Software, Theory of Computation
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.