2. Specifying New Pure Types For Modeling

JML comes with a suite of pure types, implemented as Java classes, that can be used as conceptual models in detailed design. As mentioned above, these are found in the package org.jmlspecs.models.

Users can also create their own pure types, by giving a class or interface the pure modifier. Since these types are to be treated as purely immutable values in specifications, they must pass certain conservative checks that make sure there is no possibility of observable side-effects from using such objects.

Classes used for modeling should also have pure methods, since, in JML, the use of non-pure methods in an assertion is a type error.

An example of a pure class used for modeling is the class QueueEntry, specified in the file `QueueEntry.jml-refined' below. Since it is pure, none of the methods declared in the class can permit side-effects (each is implicitly pure). It is written in a `.jml-refined' file. Since this kind of file is understood by JML but is not a Java source code file, JML allows it to contain method specifications without bodies. The class QueueEntry has three public model fields obj, priorityLevel, and timeStamp. The invariant clause states that the priorityLevel and timeStamp fields cannot be negative in a client-visible state.

package org.jmlspecs.samples.jmlkluwer; import org.jmlspecs.models.JMLType; public /*@ pure @*/ class QueueEntry implements JMLType { //@ public model Object obj; //@ public model int priorityLevel; //@ public model long timeStamp; /*@ public invariant @ priorityLevel >= 0 && timeStamp >= 0; @*/ /*@ public normal_behavior @ requires argLevel >= 0 && argTimeStamp >= 0; @ assignable obj, priorityLevel, timeStamp; @ ensures obj == argObj && priorityLevel == argLevel @ && timeStamp == argTimeStamp; @*/ public QueueEntry(Object argObj, int argLevel, long argTimeStamp); /*@ also @ public normal_behavior @ ensures \result instanceof QueueEntry; @ ensures_redundantly this.equals(\result); @*/ public Object clone(); /*@ also @ public normal_behavior @ old QueueEntry oldo = (QueueEntry)o; @ requires o instanceof QueueEntry; @ ensures \result <==> @ oldo.obj == obj @ && oldo.priorityLevel == priorityLevel @ && oldo.timeStamp == timeStamp; @ also @ public normal_behavior @ requires !(o instanceof QueueEntry); @ ensures \result == false; @*/ public boolean equals(/*@ nullable @*/ Object o); //@ ensures \result == priorityLevel; public int getLevel(); //@ ensures \result == obj; public Object getObj(); }

In the above specification, the constructor's specification follows the invariant. The constructor takes three arguments and initializes the fields from them. The precondition of this constructor states that it can only be called if the argObj argument is not null; if this were not true, then the invariant would be violated.

The clone and equals methods in QueueEntry are related to the interface JMLType, which QueueEntry extends. In JML when a class implements an interface, it inherits the specifications of that interface. The interface JMLType specifies just these two methods. The specifications of these methods are thus inherited by QueueEntry, and thus the specifications given here add to the given specifications. The specification of the method clone in JMLType (quoted from [Leavens-Baker-Ruby01]) is as follows.

/*@ also @ public normal_behavior @ ensures \result instanceof JMLType @ && ((JMLType)\result).equals(this); @*/ public /*@ pure @*/ Object clone();

The above specification says that, for JMLType objects, clone cannot throw exceptions, and its result must be a JMLType object, with the same value as this. (In Java, this names the receiver of a method call).

Inheritance of method specifications means that an implementation of clone must satisfy both the inherited specification from JMLType and the given specification in QueueEntry. The meaning of the method inheritance in this example is shown in below [Dhara-Leavens96]. (The modifier pure from the superclass can be added in here, although it is redundant for a method of a pure class.)

/*@ also @ public normal_behavior @ ensures \result instanceof JMLType @ && ((JMLType)result).equals(this); @ also @ public normal_behavior @ ensures \result instanceof QueueEntry; @ ensures_redundantly @ ((QueueEntry)\result).equals(this); @*/ public /*@ pure @*/ Object clone();

Satisfying both of the cases is possible because QueueEntry is a subtype of JMLType, and because JML interprets the meaning of E1.equals(E2) using the run-time class of E1.

The ensures_redundantly clause allows the specifier to state consequences of the specification that follow from its meaning [Leavens-Baker99] [Tan94] [Tan95]. In this case the predicate given follows from the inherited specification and the one given. This example shows a good use of such redundancy: to highlight important inherited properties for the reader of the (original, unexpanded) specification.

Case analysis is used again in the specification of QueueEntry's equals method. As before, the behavior must satisfy each case of the specification. That is, when the argument o is an instance of type QueueEntry, the first case's postcondition must be satisfied, otherwise the result must be false. The nullable annotation is needed on the argument type for the equals method, because the argument o is allowed to be null by the Java documentation. Without this nullable annotation, JML would implicitly add a precondition that the formal o must be non-null [Chalin-Rioux05].