5. Related Work

Our general design strategy for making JML practical and effective has been to blend the Eiffel [Meyer92a] [Meyer92b] [Meyer97] and Larch [Guttag-Horning93] [LeavensLarchFAQ] [Wing87] [Wing90a] approaches to specification. From Eiffel we have used the idea that assertions are written using Java's expression syntax as much as possible, thereby avoiding large amounts of special-purpose logical notations. JML also adapts the \old notation from Eiffel, instead of the Larch style annotation of names with state functions. Currently JML does not come with tools to execute preconditions to help debug programs, as in Eiffel. We plan to eventually extend JML's tools to support the testing of postconditions at run-time as well.

However, Eiffel specifications, as written by Meyer, are typically not as complete as model-based specifications written, for example, in Larch BISLs or VDM [Jones90]. For example, Meyer partially specifies a remove (i.e., pop) method for stacks as requiring that the stack not be empty, and ensuring that the stack value in the post-state has one fewer items than in the pre-state (see p. 339 of [Meyer97]). However, the only characterization of which item is removed is given informally as a comment. Nothing is said formally that ensures that the other elements of the stack are unchanged. To allow more complete specifications, we need ideas from model-based specification languages.

JML's semantic differences from Eiffel (and its cousins Sather and Sather-K) allow one to more easily write more complete specifications, following the ideas of model-based specification languages. The most important of these is JML's use of specification-only declarations. These model declarations allow more abstract and exact specifications of behavior than is typically done in Eiffel. For example, because one has a model of the abstract values of stack objects, one can precisely state both which element is removed by pop and that the other elements on the stack are unchanged. The use of model fields in JML thus allows one to write specifications that are similar to the spirit of VDM or Larch BISLs.

A more minor difference from Eiffel is that in JML one can specify frame conditions, using the assignable clause. Our interpretation of the assignable clause is very strict, as even benevolent side effects are disallowed if the assignable clause is omitted [Leino95] [Leino95a].

Another difference from Eiffel is that we have extended the syntax of Java expressions with quantifiers and other constructs that are needed for logical expressiveness, but which are not always executable. Finally, we ban side-effects and other problematic features of code in assertions.

On the other hand, our experience with Larch/C++ [Leavens96b] [Leavens99] has taught us to adapt the model-based approach in two ways, with the aim of making it more practical and easy to learn. The first adaptation is again the use of specification-only model (or ghost) variables. An object will thus have (in general) several such model fields, which are used only for the purpose of describing, abstractly, the values of objects. This simplifies the use of JML, as compared with most Larch BISLs, since specifiers (and their readers) hardly ever need to know about algebraic style specification. It also makes designing a model for a Java class or interface similar, in some respects, to designing an implementation data structure in Java. We hope that this similarity will make the specification language easier to understand.

The second adaptation is hiding of the details of mathematical modeling behind a facade of Java classes. In the Larch approach to behavioral interface specification [Wing87], the mathematical notation used in assertions is presented directly to the specifier. This allows the same mathematical notation to be used in many different specification languages. However, it also means that the user of such a specification language has to learn a notation for assertions that is different than their programming language's notation for expressions. (A preliminary study by Finney [Finney96] indicates that a large number of special-purpose, graphic mathematical notations, such as those found in Z [Hayes93] [Spivey92] may make such specifications hard to read, even for programmers trained in the notation.) In JML we use a compromise approach, hiding these details behind Java classes. These classes are pure, in the sense that they reflect the underlying mathematics, and hence do not use side-effects (at least not in any observable way). Besides insulating the user of JML from the details of the mathematical notation, this compromise approach also insulates the design of JML from the details of the mathematical logic used for JML's semantics and for theorem proving. We believe that the use of slightly extended Java notation for assertions is appropriate, given that JML is used in detailed design, and thus will mostly be read and written by persons familiar with Java.