4. Other Features of JML

Following Leino [Leino98], JML uses data groups, with in and maps \into clauses to relate model fields to the concrete fields of objects. For example, in the following

private ArrayList theElems; //@ in size;

the in clause says that theElems is in the data group of the model field size. This allows theElems to be assigned to whenever size is assignable, and also says that the value of size can be partly determined by theElems.

One can also use a represents clause to say how the model field size and the concrete field theElems are related. For example, the following says that the value of size is determined by calling the size() method of theElems.

private represents size <- theElems.size();

The represents clause gives additional facts that can be used in reasoning about the specification. This clause serves the same purpose as an abstraction function in various proof methods for abstract data types (such as [Hoare72a]). The represents clause above tells how to extract the value of size from the value of theElems. A represents clause has to be declared to be private if, as in this example, some variables mentioned in it are private (as is usually the case).

JML also has history constraints [Liskov-Wing94]. A history constraint is used to say how values can change between earlier and later states, such as a method's pre-state and its post-state. This prohibits subtypes from making certain state changes, even if they implement more methods than are specified in a given class. For example, the following history constraint

public constraint MAX_SIZE == \old(MAX_SIZE);

says that the value of MAX_SIZE cannot change.

JML has the ability to specify what methods a method may call, using a callable clause. This allows one to know which methods need to be looked at when overriding a method [Kiczales-Lamping92], and to apply the ideas of "reuse contracts" [Steyaert-etal96].