Go to the first, previous, next, last section, table of contents.


2. Class and Interface Specifications

In this section we give some examples of JML class specifications that illustrate the basic features of JML.

2.1 Abstract Models

A simple example of an abstract class specification is the ever-popular UnboundedStack type, which is presented below. It would appear in a file named `UnboundedStack.java'.

package org.jmlspecs.samples.stacks;

//@ model import org.jmlspecs.models.*;

public abstract class UnboundedStack {

  /*@ public model JMLObjectSequence theStack
    @       initially theStack != null && theStack.isEmpty();
    @*/

  //@ public invariant theStack != null;

  /*@ public normal_behavior
    @   requires !theStack.isEmpty();
    @   assignable theStack;
    @   ensures theStack.equals(\old(theStack.trailer()));
    @*/
  public abstract void pop( );

  /*@ public normal_behavior
    @   assignable theStack;
    @   ensures theStack.equals(\old(theStack.insertFront(x)));
    @*/
  public abstract void push(Object x);

  /*@ public normal_behavior
    @   requires !theStack.isEmpty();
    @   assignable \nothing;
    @   ensures \result == theStack.first();
    @*/
  public /*@ pure @*/ abstract Object top( );
}

The above specification contains the declaration of a model field, an invariant, and some method specifications. These are described below.

2.1.1 Model Fields

In the fourth non-blank line of `UnboundedStack.java', a model data field, theStack, is declared. Since it is declared using the JML modifier model, such a field does not have to be implemented; however, for purposes of the specification we treat much like any other Java field (i.e., as a variable location). That is, we imagine that each instance of the class UnboundedStack has such a field.

The type of the model field theStack is a type designed for mathematical modeling, JMLObjectSequence. Objects of this type are sequences of objects. This type is provided by JML in the package org.jmlspecs.models, which is imported in the second non-blank line of the figure. Note that this import declaration does not have to appear in the implementation, since it is modified by the keyword model. In general, any declaration form in Java can have this modifier, with the same meaning. That is, a model declaration is only used for specification purposes, and does not have to appear in an implementation.

At the end of the model field's declaration above is an initially clause. (Such clauses are adapted from RESOLVE [Ogden-etal94] and the refinement calculus [Back88] [Back-vonWright98] [Morgan-Vickers94] [Morgan94].) Model fields cannot be explicitly initialized (and thus cannot be final), because there is no storage directly associated with them. However, one can use an initially clause to describe an abstract initialization for a model field. Initially clauses can be attached to any field declaration, including non-model fields, and permit one to constrain the initial values of such fields. Knowing something about the initial value of the field permits data type induction [Hoare72a] [Wing83] for abstract classes and interfaces. The initially clause must appear to be true of the field's starting value. That is, all reachable objects of the type UnboundedStack must appear to have been created as empty stacks and subsequently modified using the type's methods.

2.1.2 Invariants

Following the model field declaration is an invariant. An invariant does not have to hold during the execution of an object's methods, but it must hold, for each reachable object in each publicly visible state; i.e., for each state outside of a public method or constructor's execution, and at the beginning and end of each public method's execution.(8) The figure's invariant just says that the value of theStack should never be null.

2.1.3 Method Specifications

Following the invariant are the specifications of the methods pop, push, and top. We describe the new aspects of these specifications below.

2.1.3.1 The Assignable Clause

The use of the assignable(9) clauses in the behavioral specifications of pop and push is interesting (and another difference from Eiffel). These clauses give frame conditions [Borgida-Mylopoulos-Reiter95]. In JML, the frame condition given by a method's assignable clause only permits the method to assign to a location, loc, if:

For example, push's specification says that it may only assign to theStack (and locations on which it depends). This allows push to assign to theStack (and its dependees), or to call some other method that makes such an assignment. Furthermore, push may assign to the formal parameter x itself, even though that location is not listed in the assignable clause, since x is local to the method. However, push may not assign to fields not mentioned in the assignable clause; in particular it may not assign to fields of its formal parameter x,(10) or call a method that makes such an assignment.

The design of JML is intended to allow tools to statically check the body of a method's implementation to determine whether its assignable clause is satisfied. This would be done by checking each assignment statement in the implementation to see if what is being assigned to is a location that some assignable clause permits. It is an error to assign to any other allocated, non-local location. However, to do this, a tool must conservatively track aliases and changes to objects containing the locations in question. Also, arrays can only be dynamically checked, in general.(11) Furthermore, JML will flag as an error a call to a method that would assign to locations that are not permitted by the calling method's assignable clause. It can do this using the assignable clause of the called method.

In JML, a location is modified by a method when it is allocated in both the pre-state of the method, reachable in the post-state, and has a value that is different in these two states. The pre-state of a method call is the state just after the method is called and parameters have been evaluated and passed, but before execution of the method's body. The post-state of a method call is the state just before the method returns or throws an exception; in JML we imagine that \result and information about exception results is recorded in the post-state.

Since modification only involves objects allocated in the pre-state, allocation of an object, using Java's new operator, does not itself cause any modification. Furthermore, since the fields of new objects are locations that were not allocated when the method started execution, they may be assigned to freely.

The reason assignments to local variables are permitted by the assignable clause is that a JML specification takes the client's (i.e., the caller's) point of view. From the client's point of view, the local variables in a method are newly-allocated, and thus assignments to such variables are invisible to the client. Hence, in JML, it is an error to list formal parameters, or other local variables, in the assignable clause. Furthermore, when formal parameters are used in a postcondition, JML interprets these as meaning the value initially given to the formal in the pre-state, since assignments to the formals within the method do not matter to the client.

JML's interpretation of the assignable clause does not permit either temporary side effects or benevolent side effects. A method with a temporary side effect assigns a location, does some work, and then assigns the original value back to that location. In JML, a method may not have temporary side effects on locations that it is not permitted to modify [Ruby-Leavens00]. A method has a benevolent side effect if it assigns to a location in a way that is not observable by clients. In JML, a method may not have benevolent side effects on locations that it is not permitted to modify [Leino95] [Leino95a].

Because JML's assignable clauses give permission to assign to locations, it is safe for clients to assume that only the listed locations (and their dependees) may have their values modified. Because locations listed in the assignable clause are the only ones that can be modified, we often speak of what locations a method can "modify," instead of the more precise "can assign to."

What does the assignable clause say about the modification of locations? In particular, although the "locations" for model fields and model variables cannot be directly assigned to in JML, their value is determined by the concrete fields and variables that they (ultimately) depend on. Thus, model fields and variables can be modified by assignments to their concrete dependees. So a method's assignable clause only permits the method to modify a location if:

In the specification of top, the assignable clause says that a call to top that satisfieds the precondition cannot assign to any locations. It does this by using the store-ref "\nothing." Unlike some formal specification languages (including Larch BISLs and older versions of JML), when the assignable clause is omitted in a heavyweight specification, in JML it the default store-ref for an omitted assignable clause, \everything, means that the method can assign to all locations (that could otherwise be assigned to by the method) can be modified. Such an assignable clause plays havoc with formal reasoning, and thus if one cares about verification, one should give an assignable clause explicitly if the method is not pure (see section 2.3.1 Purity).

2.1.3.2 Old Values

When a method can modify some locations, they may have different values in the pre-state and post-state of a call. Often the post-condition must refer to the values held in both of these states. JML uses a notation similar to Eiffel's to refer to the pre-state value of a variable. In JML the syntax is \old(E), where E is an expression. (Unlike Eiffel, we use parentheses following \old to delimit the expression to be evaluated in the pre-state explicitly. JML also uses backslashes (\\) to mark the keywords it uses in expressions; this avoids interfering with Java program identifiers, such as "old".)

The meaning of \old(E) is as if E were evaluated in the pre-state and that value is used in place of \old(E) in the assertion. It follows that, an expression like \old(myVar).theStack may not mean what is desired, since only the old value of myVar is saved; access to the field theStack is done in the post-state. If it is the field, theStack, not the variable, myVar, that is changing, then probably what is desired is \old(myVar.theStack). To avoid such problems, it is good practice to have the expression E in \old(E) be such that its type is either the type of a primitive value, such as an int, or a type with immutable objects, such as JMLObjectSequence.

As another example, in pop's postcondition the expression \old(theStack.trailer()) has type JMLObjectSequence, so it is immutable. The value of theStack.trailer() is computed in the pre-state of the method.

Note also that, since JMLObjectSequence is a reference type, one is required to use equals instead of == to compare them for equality of values. (Using == would be a mistake, since it would only compare them for object identity, which in combination with new would always yield false.)

2.1.3.3 Correct Implementation

The specification of push does not have a requires clause. This means that the method imposes no obligations on the caller. (The meaning of an omitted requires clause is that the method's precondition is true, which is satisfied by all states, and hence imposes no obligations on the caller.) This seems to imply that the implementation must provide a literally unbounded stack, which is surely impossible. We avoid this problem, by following Poetzsch-Heffter [Poetzsch-Heffter97] in releasing implementations from their obligations to fulfill the postcondition when Java runs out of storage. In general, a method specified with normal_behavior has a correct implementation if, whenever it is called in a state that satisfies its precondition, either

We discuss the specification of methods with exceptions in the next subsection.

2.2 Dependencies

In this subsection we present two example specifications. The two example specifications, BoundedThing and BoundedStackInterface, are used to describe how model (and concrete) fields can be related to one another, and how dependencies among them affect the meaning of the assignable clause. Along the way we also demonstrate how to specify methods that can throw exceptions and other features of JML.

2.2.1 Specification of BoundedThing

The specification in the file `BoundedThing.java', shown below, is an interface specification with a simple abstract model. In this case, there are two model fields MAX_SIZE and size.

package org.jmlspecs.samples.stacks;

public interface BoundedThing {

    //@ public model instance int MAX_SIZE;
    //@ public model instance int size;

    /*@ public instance invariant MAX_SIZE > 0;
        public instance invariant
                0 <= size && size <= MAX_SIZE;
        public instance constraint MAX_SIZE == \old(MAX_SIZE);
      @*/

    /*@  public normal_behavior
           ensures \result == MAX_SIZE;
      @*/
    public /*@ pure @*/ int getSizeLimit();

    /*@  public normal_behavior
           ensures \result <==> size == 0;
      @*/
    public /*@ pure @*/ boolean isEmpty();

    /*@  public normal_behavior
          ensures \result <==> size == MAX_SIZE;
      @*/
    public /*@ pure @*/ boolean isFull();

    /*@ also
         public behavior
           assignable \nothing;
           ensures \result instanceof BoundedThing
                  && size == ((BoundedThing)\result).size;
           signals (CloneNotSupportedException) true;
      @*/
    public Object clone () throws CloneNotSupportedException;
}

After discussing the model fields, we describe the other parts of the specification below.

2.2.1.1 Model Fields in Interfaces

In the specification above, the fields MAX_SIZE and size are both declared using the modifier instance. Because of the use of the keyword instance, these fields are thus treated as normal model fields, i.e., as an instance variable in each object that implements this interface. By default, as in Java, fields are static in interfaces, and so if instance is omitted, the field declarations would be treated as class variables. The instance keyword tells the reader that the variable being declared is not static, but has a copy in each instance of a class that implements this interface.

Java does not allow non-static fields to be declared in interfaces. However, JML allows non-static model (and ghost) fields in interfaces when one uses instance. The reason for this extension is that such fields are essential for defining the abstract values and behavior of the objects being specified.(12)

In specifications of interfaces that extend or classes that implement this interface, these model fields are inherited. Thus, every object that has a type that is a subtype of the BoundedThing interface is thought of, abstractly, as having two fields, MAX_SIZE and size, both of type int.

2.2.1.2 Invariant and History Constraint

Three pieces of class-level specification come after the abstract model in the above specification.

The first two are invariant clauses. Writing several invariant clauses in a specification, like this is equivalent to writing one invariant clause which is their conjunction. Both of these invariants are instance invariants, because they use the instance modifier. By default, in interfaces, invariants and history constraints are static, unless marked with the instance modifier. Static invariants may only refer to static fields, while instance invariants can refer to both instance and static fields.

The first invariant in the figure says that in every publicly visible state, every reachable object that is a BoundedThing must have a positive MAX_SIZE field. The second invariant says that, in each publicly visible state, every reachable object that is a BoundedThing must have a size field that is non-negative and less than or equal to MAX_SIZE.

Following the invariants is a history constraint [Liskov-Wing94]. Like the invariants, it uses the modifier instance, because it refers to instance fields. A history constraint is used to say how values can change between earlier and later publicly-visible states, such as a method's pre-state and its post-state. This prohibits subtype objects from making certain state changes, even if they implement more methods than are specified in a given class. The history constraint in the specification above says that the value of MAX_SIZE cannot change, since in every pre-state and post-state, its value in the post-state, written MAX_SIZE, must equal its value in the pre-state, written \old(MAX_SIZE).

2.2.1.3 Details of the Method Specifications

Following the history constraint are the interfaces and specifications for four public methods. Notice that, if desired, the at-signs (@) may be omitted from the left sides of intermediate lines, as we do in this specification.

The use of == in the method specifications is okay, since in each case, the things being compared are primitive values, not references. The notation <==> can be read "if and only if". It has the same meaning for Boolean values as ==, but has a lower precedence. Therefore, the expression "\result <==> size == 0" in the postcondition of the isEmpty method means the same thing as "\result == (size == 0)".

2.2.1.4 Adding to Method Specifications

The specification of the last method of BoundedThing, clone, is interesting. Note that it begins with the keyword also. This form is intended to tell the reader that the specification given is in addition to any specification that might have been given in the superclass Object, where clone is declared as a protected method. A form like this must be used whenever a specification is given for a method that overrides a method in a superclass, or that implements a method from an implemented interface.

2.2.1.5 Specifying Exceptional Behavior

The specification of clone also uses behavior instead of normal_behavior. In a specification that starts this way, one can describe not just the case where the execution returns normally, but also executions where exceptions are thrown. In such a specification, the conditions under which exceptions can be thrown can be described by the predicate in the signals clauses,(13) and the conditions under which the method may return without throwing an exception are described by the ensures clause. In this specification, the clone method may always throw the exception, because it only needs to make the predicate "true" true to do so. When the method returns normally, it must make the given postcondition true.

In JML, a normal_behavior specification can be thought of as a syntactic sugar for a behavior specification to which the following clause is added [Raghavan-Leavens00].

     signals (java.lang.Exception) false;

This formalizes the idea that a method with a normal_behavior specification may not throw an exception when the specification's precondition is satisfied.

JML also has a specification form exceptional_behavior, which can be used to specify when exceptions must be thrown. A specification that uses exceptional_behavior can be thought of as a syntactic sugar for a behavior specification to which the following clause is added [Raghavan-Leavens00].

     ensures false;

This formalizes the idea that a method with a exceptional_behavior specification may not return normally when the specification's precondition is satisfied.

Since in the specification of clone, we want to allow the implementation to make a choice between either returning normally or throwing an exception, and we do not wish to distinguish the preconditions under which each choice must be made, we cannot use either of the more specialized forms normal_behavior or exceptional_behavior. Thus the specification of clone demonstrates the somewhat unusual case when the more general form of a behavior specification is needed.

Finally note that in the specification of clone, the postcondition says that the result will be a BoundedThing and that its size will be the same as the model field size. The use of the cast in this postcondition is necessary, since the type of \result is Object. (This also adheres to our goal of using Java syntax and semantics to the extent possible.) Note also that the conjunct \result instanceof BoundedThing "protects" the next conjunct [Leavens-Wing97a] since if it is false the meaning of the cast does not matter.

2.2.2 Specification of BoundedStackInterface

The specification in the file `BoundedStackInterface.java' below gives an interface for bounded stacks that extends the interface for BoundedThing. Note that this specification can refer to the instance fields MAX_SIZE and size inherited from the BoundedThing interface.

package org.jmlspecs.samples.stacks;
//@ model import org.jmlspecs.models.*;
public interface BoundedStackInterface extends BoundedThing {
  /*@ public model instance JMLObjectSequence theStack
    @             initially theStack != null && theStack.isEmpty();
    @*/
  //@ public instance depends size <- theStack;
  //@ public instance represents size <- theStack.length();
  /*@ public instance invariant theStack != null;
    @ public instance invariant_redundantly
    @                           theStack.length() <= MAX_SIZE;
    @ public instance invariant 
    @         (\forall int i; 0 <= i && i < theStack.length();
    @                         theStack.itemAt(i) != null);
    @*/

  /*@   public normal_behavior
    @     requires !theStack.isEmpty();
    @     assignable size, theStack;
    @     ensures theStack.equals(\old(theStack.trailer()));
    @ also
    @   public exceptional_behavior
    @     requires theStack.isEmpty();
    @     assignable \nothing;
    @     signals (BoundedStackException);
    @*/
  public void pop( ) throws BoundedStackException;

  /*@   public normal_behavior
    @     requires theStack.length() < MAX_SIZE && x != null;
    @     assignable size, theStack;
    @     ensures theStack.equals(\old(theStack.insertFront(x)));
    @     ensures_redundantly theStack != null && top() == x
    @              && theStack.length() == \old(theStack.length()+1);
    @ also
    @   public exceptional_behavior
    @     requires theStack.length() >= MAX_SIZE || x == null;
    @     assignable \nothing;
    @     signals (BoundedStackException)
    @                  theStack.length() == MAX_SIZE;
    @     signals (NullPointerException) x == null;
    @*/
  public void push(Object x )
         throws BoundedStackException, NullPointerException;

  /*@   public normal_behavior
    @     requires !theStack.isEmpty();
    @     ensures \result == theStack.first() && \result != null;
    @ also
    @   public exceptional_behavior
    @     requires theStack.isEmpty();
    @     signals (BoundedStackException e)
    @             \fresh(e) && e != null
    @           && e.getMessage().equals("empty stack");
    @     signals_redundantly (BoundedStackException);
    @*/
  public /*@ pure @*/ Object top( ) throws BoundedStackException;
}

The abstract model for BoundedStackInterface adds to the inherited model by declaring a model instance field named theStack. This field is typed as a JMLObjectSequence.

In the following we describe how the new model instance field, theStack, is related to size from BoundedThing. We also use this example to explain more JML features.

2.2.2.1 Depends and Represents Clauses

The depends and represents clauses that follow the declaration of theStack are an important feature in modeling with layers of model fields.(14) They also play a crucial role in relating model fields to the concrete fields of objects, which can be considered to be the final layer of detail in a design.

The depends clause in BoundedStackInterface says that size depends on theStack; this means that size might change its value when the theStack changes. Another way of looking at this is that, if one wants to change size, this can be done by changing theStack. We also say that theStack is a dependee of size.

A model field can be declared to depend on another model field or on a concrete field (i.e., a field that is not a model field). However, concrete fields cannot be declared to depend on other fields.

The depends clause is important in "loosening up" the assignable clause, for example to permit the fields of an object that implement the abstract model to be changed [Leino95] [Leino95a]. This "loosening up" also applies to model fields that have dependencies declared. For example, since size depends on theStack, whenever size is mentioned in a assignable clause, then theStack is implicitly allowed to be modified.(15) Thus it is only for rhetorical purposes that we mention both size and theStack in the assignable clauses of pop and push. Note, however, that just mentioning theStack would not permit size to be modified, because theStack does not depend on size.

The represents clause in BoundedStackInterface says how the value of size is related to the value of theStack. It says that the value of size is theStack.length().

A represents clause gives additional facts that can be used in reasoning about the specification. It serves the same purpose as an abstraction function in various proof methods for abstract data types (such as [Hoare72a]).

One can only use a represents clause to state facts about a field and its dependees. To state relationships among concrete data fields or on fields that are not related by a dependency, one should use an invariant.

2.2.2.2 Redundant Specification

The second invariant clause that follows the represents clause in the specification of BoundedStackInterface above is our first example of checkable redundancy in a specification [Leavens-Baker99] [Tan94] [Tan95]. This concept is signaled in JML by the use of the suffix _redundantly on a keyword (as in ensures_redundantly). It says both that the stated property is specified to hold and that this property is believed to follow from the other properties of the specification. In this case the redundant invariant follows from the given invariant, the invariant inherited from the specification of BoundedThing, and the fact stated in the represents clause. Even though this invariant is redundant, it is sometimes helpful to state such properties, to bring them to the attention of the readers of the specification.

Checking that such claimed redundancies really do follow from other information is also a good way to make sure that what is being specified is really what is intended. Such checks could be done manually, during reviews, or with the aid of a theorem prover. JML's runtime assertion checker can also check such redundant specifications, but, of course, can only find examples where they do not hold.

2.2.2.3 Multiple Specification Cases

Following the redundant invariant of BoundedStackInterface are the specifications of the pop, push, and top methods. These are interesting for several new features that they present. Each of these has both a normal and exceptional behavior specified. The meaning of such multiple specification cases is that, when the precondition of one of them is satisfied, the rest of that specification case must also be obeyed.

A specification with several specification cases is shorthand for one in which the separate specifications are combined [Dhara-Leavens96] [Leavens97c] [Wing83] [Wills94]. The desugaring can be thought of as proceeding in two steps (see [Raghavan-Leavens00] for more details). First, the public normal_behavior and public exceptional_behavior cases are converted into public behavior specifications as explained above. This would produce a specification for pop as shown below. The use of implies_that introduces a redundant specification that can be used, as is done here, to point out consequences of the specification to the reader. In this case the specification in question is the one mentioned in the refine clause. Note that in the second specification case of the figure below, the signals clause has been expanded to include the implicit predicate "true"; this "true" was omitted from the original specification, since such a use of the signals clause is common enough for JML to allow it to be omitted.

//@ refine "BoundedStackInterface.java";

public interface BoundedStackInterface extends BoundedThing {
  /*@ also
    @ implies_that
    @   public behavior
    @     requires !theStack.isEmpty();
    @     assignable size, theStack;
    @     ensures theStack.equals(\old(theStack.trailer()));
    @     signals (java.lang.Exception) false;
    @  also
    @   public behavior
    @     requires theStack.isEmpty();
    @     assignable \nothing;
    @     ensures false;
    @     signals (BoundedStackException) true;
    @*/
  public void pop( ) throws BoundedStackException;
}    

The second step of the desugaring is shown below. As can be seen from this example, public behavior specifications that are joined together using also have a precondition that is the disjunction of the preconditions of the combined specification cases. The assignable clause for the expanded specification is the union of all the assignable clauses for the cases, with each modification governed by the corresponding precondition (which follows the keyword if). That is, variables are only allowed to be modified if the modification was permitted in the corresponding case, as determined by its precondition. The ensures clauses of the second desugaring step correspond to the ensures clauses for each specification case; they say that whenever the precondition for that specification case held in the pre-state, its postcondition must also hold. As can be seen in the specification below, in logic this is written using an implication between \old wrapped around the case's precondition and its postcondition. Having multiple ensures clauses is equivalent to writing a single ensures clause that has as its postcondition the conjunction of the given postconditions. Similarly, the signals clauses in the desugaring correspond to those in the given specification cases; as for the ensures clauses, each has a predicate that says that signaling that exception can only happen when the predicate in that case's precondition holds.

//@ refine "BoundedStackInterface.jml";
public interface BoundedStackInterface extends BoundedThing {
  /*@ also
    @ implies_that
    @   public behavior
    @     requires !theStack.isEmpty() || theStack.isEmpty();
    @     assignable size if !theStack.isEmpty(),
    @                 theStack if !theStack.isEmpty();
    @     ensures \old(!theStack.isEmpty())
    @               ==> theStack.equals(\old(theStack.trailer()));
    @     ensures \old(theStack.isEmpty()) ==> false;
    @     signals (java.lang.Exception)
    @              \old(!theStack.isEmpty()) ==> false;
    @     signals (BoundedStackException)
    @              \old(theStack.isEmpty()) ==> true;
    @*/
  public void pop( ) throws BoundedStackException;
}

In the file `BoundedStackInterface.refines-java' above, the precondition of pop reduces to true. However, the precondition shown is the general form of the expansion. Similar remarks apply to other predicates.

Finally, note how, as in the specification of top, one can specify more details about the exception object thrown. The exceptional behavior for top says that the exception object thrown, e, must be freshly allocated, non-null, and have the given message.

2.2.2.4 Pitfalls in Specifying Exceptions

A particularly interesting example of multiple specification cases occurs in the specification of the BoundedStackInterface's push method. Like the other methods, this example has two specification cases; one of these is a normal_behavior and one is an exceptional_behavior. However, the exceptional behavior of push is interesting because it specifies more than one exception that may be thrown. The requires clause of the exceptional behavior says that an exception must be thrown when either the stack cannot grow larger, or when the argument x is null. The first signals clause says that, if a BoundedStackException is thrown, then the stack cannot grow larger, and the second signals clause says that, if a NullPointerException is thrown, then x must be null. The specification is written in this way because it may be that both conditions occur; when that is the case, the specification allows the implementation to choose (even nondeterministically) which exception is thrown.

Specifiers should be wary of such situations, where two exceptional conditions may both be true simultaneously, because it is impossible in Java to throw more than one exception from a method call. Thus, for example, if the specification of push had been written as follows, it would not be implementable.(16) The problem is that both exceptional preconditions may be true, and in that case an implementation cannot throw both exceptions.

  /*@   public normal_behavior
    @     requires theStack.length() < MAX_SIZE && x != null;
    @     assignable size, theStack;
    @     ensures theStack.equals(\old(theStack.insertFront(x)));
    @     ensures_redundantly theStack != null && top() == x
    @              && theStack.length() == \old(theStack.length()+1);
    @ also
    @   public exceptional_behavior
    @     requires theStack.length() >= MAX_SIZE;
    @     assignable \nothing;
    @     signals (BoundedStackException);
    @ also                                   // this is wrong!
    @   public exceptional_behavior
    @     requires x == null;
    @     assignable \nothing;
    @     signals (NullPointerException);
    @*/
  public void push(Object x )
         throws BoundedStackException, NullPointerException;

One could fix the example above by writing one of the requires clauses in the two exceptional behaviors to exclude the other, although this would make the specification deterministic about which exception would be thrown when both exceptional conditions occur. In general, it seems best to avoid this pitfall by writing several exceptional cases together in a single exceptional behavior clause, as was done originally for push (see section 2.2.2.3 Multiple Specification Cases) or to simply use a single behavior clause. One can also use a lightweight specification, which is like using a single behavior clause, but with different defaults.

2.2.2.5 Redundant Ensures Clauses

Finally, there is more redundancy in the specifications of push in the original specification of BoundedStackInterface above, which has a redundant ensures clause in its normal behavior. For an ensures_redundantly clause, what one checks is that the conjunction of the precondition, the meaning of the assignable clause, and the (non-redundant) postcondition together imply the redundant postcondition. It is interesting to note that, for push, the specifications for stacks written in Eiffel (see page 339 of [Meyer97]) expresses just what we specify in push's redundant postcondition. This conveys strictly less information than the non-redundant postcondition for push's normal behavior, since it says little about the elements of the stack.(17)

2.3 Types For Modeling

JML comes with a suite of types with immutable objects and pure methods, that can be used for defining abstract models. These are found in the package org.jmlspecs.models, which includes both collection and non-collection types (such as JMLInteger) and a few auxiliary classes (such as exceptions and enumerators).

The collection types in this package can hold either objects or values; this distinction determines the notion of equality used on their elements and whether cloning is done on the elements. The object collections, such as JMLObjectSet and JMLObjectBag, use == and do not clone. The value collections, such as JMLValueSet and JMLValueBag, use .equals to compare elements, and clone the objects added to and returned from them. The objects in a value collection are representatives of equivalence classes (under .equals) of objects; their values matter, but not their object identities. By contrast an object container contains object identities, and the values in these objects do not matter.

Simple collection types include the set types, JMLObjectSet and JMLValueSet, and sequence types JMLObjectSequence and JMLValueSequence. The binary relation and map types can independently have objects in their domain or range. The binary relation types are named JMLObjectToObjectRelation, JMLObjectToValueRelation, and so on. For example, JMLObjectToValueRelation is a type of binary relations between objects (not cloned and compared using ==) and values (which are cloned and compared using .equals). The four map types are similarly named according to the scheme JML...To...Map.

Users can also create their own types with pure methods for mathematical modeling if desired. Since pure methods may be used in assertions, they must be declared with the modifier pure and pass certain conservative checks that make sure there is no possibility of observable side-effects from their use. We discuss purity and give several examples of such types below.

2.3.1 Purity

We say a method is pure if it is either specified with the modifier pure or is a non-static method that appears in the specification of a pure interface or class. Similarly, a constructor is pure if it is either specified with the modifier pure or appears in the specification of a pure class.

A pure method that is not a constructor implicitly has a specification that does not allow any side-effects. That is, its specification refines (i.e., is stronger than) the following(18):

        behavior
           assignable \nothing;

A pure constructor implicitly has a specification that only allows it to assign to the non-static fields of the class in which it appears (including those inherited from its superclasses and model instance fields from the interfaces that implements).

Implementations of pure methods and constructors will be checked to see that they meet these conditions on what locations they can assign to. To make such checking modular, a pure method or constructor implementation is prohibited from calling methods or constructors that are not pure.

A pure method or constructor must also be provably terminating.(19) Recursion is permitted, both in the implementation of pure methods and the data structures they manipulate, and in the specifications of pure methods. When recursion is used in a specification, the proof of well-formedness for the specification involves the use of JML's measured_by clause.

Since a pure method may not go into an infinite loop, if it has a non-trivial precondition, it should throw an exception when its normal precondition is not met. This exceptional behavior does not have to be specified or programmed explicitly, but technically there is an obligation to meet the specification that the method never loops forever.

A pure method can be declared in any class or interface, and a pure constructor can be declared in any class. JML will specify the pure methods and constructors in the standard Java libraries as pure.

As a convenience, instead of writing pure on each method declared in a class and interface, one can use the modifier pure on classes and interfaces and classes. This simply means that each non-static method and each constructor declared in such a class or interface is pure. Note that this does not mean that all methods inherited (but not declared in and hence not overridden in) the class or interface are pure. For example, every class inherits ultimately from java.lang.Object, which has some methods, such as notify and notifyAll that are manifestly not pure. Thus each class will have some methods that are not pure. Despite this, it is convenient to refer to classes and interfaces declared with the pure modifier as pure.

In JML the modifiers model and pure are orthogonal. (Recall something declared with the modifier model does not have to be implemented, and is used purely for specification purposes.) Therefore, one can have a model method that is not pure (these might be useful in JML's model programs) and a pure method that is not a model method. Nevertheless, usually a model method (or constructor) should be pure, since there is no way to use non-pure methods in an assertion, and model methods cannot be used in normal Java code.

By the same reasoning, model classes should, in general, also be pure. Model classes cannot be used in normal Java code, and hence their methods are only useful in assertions (and JML's model programs). Hence it is typical, although not required, that a model class also be a pure class. We give some examples of pure interfaces, abstract classes, and classes below.

2.3.2 Money

The following example begins a specification of money that would be suitable for use in abstract models. Our specification is rather artificially broken up into pieces to allow each piece to have a specification that fits on a page. This organization is not necessarily something we would recommend, but it does give us a chance to illustrate more features of JML.

Consider first the interface Money specified below. The abstract model here is a single field of the primitive Java type long, which holds a number of pennies. Note that the declaration of this field, pennies, again uses the JML keyword instance.

package org.jmlspecs.samples.prelimdesign;

import org.jmlspecs.models.JMLType;

public /*@ pure @*/ interface Money extends JMLType
{
  //@ public model instance long pennies;

  //@ public instance constraint pennies == \old(pennies);

  /*@     public normal_behavior
    @       assignable \nothing;
    @       ensures \result == pennies / 100;
    @ for_example
    @     public normal_example
    @       requires pennies == 703;
    @       assignable \nothing;
    @       ensures \result == 7;
    @   also
    @     public normal_example
    @       requires pennies == 799;
    @       assignable \nothing;
    @       ensures \result == 7;
    @   also
    @     public normal_example
    @       requires pennies == -503;
    @       assignable \nothing;
    @       ensures \result == -5;
    @*/
  public long dollars();

  /*@   public normal_behavior
    @     assignable \nothing;
    @     ensures \result == pennies % 100;
    @ for_example
    @     requires pennies == 703;
    @     assignable \nothing;
    @     ensures \result == 3;
    @   also
    @     requires pennies == -503;
    @     assignable \nothing;
    @     ensures \result == -3;
    @*/
  public long cents();

  /*@ also
    @   public normal_behavior
    @     assignable \nothing;
    @     ensures \result <==> o2 instanceof Money
    @                           && pennies == ((Money)o2).pennies;
    @*/
  public boolean equals(Object o2);

  /*@ also
    @   public normal_behavior
    @     assignable \nothing;
    @     ensures \result instanceof Money
    @       && ((Money)\result).pennies == pennies;
    @*/
  public Object clone();
}

This interface has a history constraint, which says that the number of pennies in an object cannot change.(20)

The following explain more aspects of JML related to the above specification.

2.3.2.1 Redundant Examples

The interesting aspect of Money's method specifications is another kind of redundancy. This new form of redundancy is examples, which follow the keyword "for_example".

Individual examples are given by normal_example clauses (adapted from our previous work on Larch/C++ [Leavens96b] [Leavens-Baker99]). Any number of these(21) can be given in a specification. In the specification of Money above there are three normal examples given for dollars and two in the specification of cents.

The specification in each example should be such that:

Requiring equivalence to the example's postcondition means that it can serve as a test oracle for the inputs described by the example's precondition. If there is only one specified public normal_behavior clause and if there are no preconditions and assignable clauses, then the example's postcondition should the equivalent to the conjunction of the example's precondition and the postcondition of the public normal_behavior specification. Typically, examples are concrete, and serve to make various rhetorical points about the use of the specification to the reader. (Exercise: check all the examples given!)

2.3.2.2 JMLType and Informal Predicates

The interface Money is specified to extend the interface JMLType. This interface is given below. Classes that implement this interface must have pure equals and clone methods with the specified behavior. The methods specified override methods in the class Object, and so they use the form of specification that begins with the keyword "also".

package org.jmlspecs.models;

/** Objects with a clone and equals method.
 * JMLObjectType and JMLValueType are refinements
 * for object and value containers (respectively).
 * @version $Revision: 1.12 $
 * @author Gary T. Leavens
 * @author Albert L. Baker
 * @see JMLObjectType
 * @see JMLValueType
 */
public interface JMLType extends Cloneable, java.io.Serializable {

    /** Return a clone of this object.
     */
    /*+@ also
      @   public normal_behavior
      @     ensures \result != null;
      @     ensures \result instanceof JMLType;
      @     ensures ((JMLType)\result).equals(this);
      @+*/
    //+@ implies_that
    /*@    ensures \result != null
      @        && \typeof(\result) <: \type(JMLType);
      @*/
    public /*+@ pure @+*/ Object clone();    

    /** Test whether this object's value is equal to the given argument.
     */
    /*+@ also
      @   public normal_behavior
      @     ensures \result ==>
      @             ob2 != null
      @             && (* ob2 is not distinguishable from this,
      @                   except by using mutation or == *);
      @ implies_that
      @   public normal_behavior
      @   {|
      @      requires ob2 != null && ob2 instanceof JMLType;
      @      ensures ((JMLType)ob2).equals(this) == \result;
      @    also
      @      requires ob2 == this;
      @      ensures \result <==> true;
      @   |}
      @+*/
    public /*+@ pure @+*/ boolean equals(Object ob2);    

    /** Return a hash code for this object.
     */
    public /*+@ pure @+*/ int hashCode();
}

The specification of JMLType is noteworthy in its use of informal predicates [Leavens96b]. In JML these start with an open parenthesis and an asterisk (`(*') and continue until a matching asterisk and closing parenthesis (`*)'). In the public specification of equals, the normal_behavior's ensures clause uses an informal predicate as an escape from formality. The use of informal predicates avoids the delicate issues of saying formally what observable aliasing means, and what equality of values means in general.(22)

In the implies_that section of the specification of the equals method is a nested case analysis, between {| and |}. The meaning of this is that each pre- and postcondition pair has to be obeyed. The first of these nested pairs is essentially saying that equals has to be symmetric. The second of these is saying that it has to be reflexive.

The implies_that section of the clone method states some implications of the specification given that are useful for ESC/Java. These repeat, from the first part of clone's specification, that the result must not be null, and that the result's dynamic type, \typeof(\result), must be a subtype of (written <:) the type JMLType.

ESC/Java understands only annotations written between the annotation markers /*@ and @*/ and on annotation comment lines of that start with //@. It does not understand annotations written between the annotation markers /*+@ and @+*/ and on annotation comment lines of that start with //+@.(23) This makes it possible for the user of JML to write specifications that can be read by both JML's tools and by ESC/Java, since JML understands (essentially) a superset of the syntax that ESC/Java understands.

2.3.3 MoneyComparable and MoneyOps

The type Money lacks some useful operations. The extensions below provide specifications of comparison operations and arithmetic, respectively.

The specification in file `MoneyComparable.java' is interesting because each of the specified preconditions protects the postcondition from undefinedness in the postcondition [Leavens-Wing97a]. For example, if the argument m2 in the greaterThan method were null, then the expression m2.pennies would not be defined.

package org.jmlspecs.samples.prelimdesign;

public /*@ pure @*/ interface MoneyComparable extends Money
{
  /*@ public normal_behavior
    @   requires m2 != null;
    @   assignable \nothing;
    @   ensures \result <==> pennies > m2.pennies;
    @*/
  public boolean greaterThan(Money m2);

  /*@ public normal_behavior
    @   requires m2 != null;
    @   assignable \nothing;
    @   ensures \result <==> pennies >= m2.pennies;
    @*/
  public boolean greaterThanOrEqualTo(Money m2);

  /*@ public normal_behavior
    @   requires m2 != null;
    @   assignable \nothing;
    @   ensures \result <==> pennies < m2.pennies;
    @*/
  public boolean lessThan(Money m2);

  /*@ public normal_behavior
    @   requires m2 != null;
    @   assignable \nothing;
    @   ensures \result <==> pennies <= m2.pennies;
    @*/
  public boolean lessThanOrEqualTo(Money m2);
}

The interface specified in the file `MoneyOps.java' below extends the interface specified above. MoneyOps is interesting for the use of its pure model methods: inRange, can_add, and can_scaleBy. These methods cannot be invoked by Java programs; that is, they would not appear in the Java implementation. When, for example inRange is called in a predicate it is equivalent to using some correct implementation of its specification. The specification of inRange also makes use of a local specification variable declaration, which follows the keyword "old". Such declarations allow one to abbreviate long expressions, or, to make rhetorical points by naming constants, as is done with epsilon. These old declarations are treated as locations that are initialized to the pre-state value of the given expression. Model methods can be normal (instance) methods as well as static (class) methods.

package org.jmlspecs.samples.prelimdesign;

public /*@ pure @*/ interface MoneyOps extends MoneyComparable
{
  /*@  public normal_behavior
    @     old double epsilon = 1.0;
    @     assignable \nothing;
    @     ensures \result <==> Long.MIN_VALUE + epsilon < d
    @                           && d < Long.MAX_VALUE - epsilon;
    @ public model boolean inRange(double d);
    @
    @  public normal_behavior
    @     requires m2!= null;
    @     assignable \nothing;
    @     ensures \result <==> inRange((double) pennies + m2.pennies);
    @ public model boolean can_add(Money m2);
    @
    @  public normal_behavior
    @     ensures \result <==> inRange(factor * pennies);
    @ public model boolean can_scaleBy(double factor);
    @*/

  /*@   public normal_behavior
    @     requires m2 != null && can_add(m2);
    @     assignable \nothing;
    @     ensures \result != null
    @           && \result.pennies == this.pennies + m2.pennies;
    @ for_example
    @   public normal_example
    @     requires this.pennies == 300 && m2.pennies == 400;
    @     assignable \nothing;
    @     ensures \result != null && \result.pennies == 700;
    @*/
  public MoneyOps plus(Money m2);

  /*@   public normal_behavior
    @     requires m2 != null
    @            && inRange((double) pennies - m2.pennies);
    @     assignable \nothing;
    @     ensures \result != null
    @           && \result.pennies == this.pennies - m2.pennies;
    @ for_example
    @   public normal_example
    @     requires this.pennies == 400 && m2.pennies == 300;
    @     assignable \nothing;
    @     ensures  \result != null && \result.pennies == 100;
    @*/
  public MoneyOps minus(Money m2);

  /*@   public normal_behavior
    @     requires can_scaleBy(factor);
    @     assignable \nothing;
    @     ensures \result != null
    @           && \result.pennies == (long)(factor * pennies);
    @ for_example
    @   public normal_example
    @     requires pennies == 400 && factor == 1.01;
    @     assignable \nothing;
    @     ensures \result != null && \result.pennies == 404;
    @*/
  public MoneyOps scaleBy(double factor);
}

Note also that JML uses the Java semantics for mixed-type expressions. For example in the ensures clause of the above specification of plus, m2.pennies is implicitly coerced to a double-precision floating point number, as it would be in Java.

2.3.4 MoneyAC

The key to proofs that an implementation of a class or interface specification is correct lies in the use of depends and represents clauses [Hoare72a] [Leino95].

Consider, for example, the abstract class specified in the file `MoneyAC.java' below. This class is abstract and has no constructors. The class declares a concrete field numCents, which is related to the model instance field pennies by the represents clause.(24) The represents clause states that the value of pennies is the value of numCents. This allows relatively trivial proofs of the correctness of the dollars and cents methods, and is key to the proofs of the other methods.

package org.jmlspecs.samples.prelimdesign;

public /*@ pure @*/ abstract class MoneyAC implements Money {

  protected long numCents;
  //@ protected depends pennies <- numCents;
  //@ protected represents pennies <- numCents;

  //@ protected constraint_redundantly numCents == \old(numCents);

  public long dollars()
  {
    return numCents / 100;
  }

  public long cents()
  {
    return numCents % 100;
  }

  public boolean equals(Object o2)
  {
    try {
      Money m2 = (Money)o2;
      return numCents == (100 * m2.dollars() + m2.cents());
    } catch (ClassCastException e) {
      return false;
    }
  }

  public Object clone()
  {
    return this;
  }
}

2.3.5 MoneyComparableAC

The straightforward implementation of the pure abstract subclass MoneyComparableAC is given below. Besides extending the class MoneyAC, it implements the interface MoneyComparable. Note that the model and concrete fields are both inherited by this class.

package org.jmlspecs.samples.prelimdesign;

public /*@ pure @*/ abstract class MoneyComparableAC
    extends MoneyAC implements MoneyComparable
{
  protected static long totalCents(Money m2)
  {
    long res = 100 * m2.dollars() + m2.cents();
    //@ assert res == m2.pennies;
    return res;
  }

  public boolean greaterThan(Money m2)
  {
    return numCents > totalCents(m2);
  }

  public boolean greaterThanOrEqualTo(Money m2)
  {
    return numCents >= totalCents(m2);
  }

  public boolean lessThan(Money m2)
  {
    return numCents < totalCents(m2);
  }

  public boolean lessThanOrEqualTo(Money m2)
  {
    return numCents <= totalCents(m2);
  }
}

An interesting feature of the class MoneyComparableAC is the protected static method named totalCents. For this method, we give its code with an embedded assertion, written following the keyword assert.(25)

Note that the model method, inRange is not implemented, and does not need to be implemented to make this class correctly implement the interface MoneyComparable.

2.3.6 USMoney

Finally, a concrete class implementation is given in the file `USMoney.java' shown below. The class USMoney implements the interface MoneyOps. Note that specifications as well as code are given for the constructors.

package org.jmlspecs.samples.prelimdesign;

public /*@ pure @*/ class USMoney
                extends MoneyComparableAC implements MoneyOps
{
  /*@   public normal_behavior
    @     assignable pennies;
    @     ensures pennies == cs;
    @ implies_that
    @   protected normal_behavior
    @     assignable pennies, numCents;
    @     ensures numCents == cs;
    @*/
  public USMoney(long cs)
  {
    numCents = cs;
  }

  /*@ public normal_behavior
    @   assignable pennies;
    @   ensures pennies == (long)(100.0 * amt);
    @   ensures_redundantly (* pennies holds amt dollars *);  @*/
  public USMoney(double amt)
  {
    numCents = (long)(100.0 * amt);
  }

  public MoneyOps plus(Money m2)
  {
    //@ assume m2 != null;
    return new USMoney(numCents + totalCents(m2));
  }

  public MoneyOps minus(Money m2)
  {
    //@ assume m2 != null;
    return new USMoney(numCents - totalCents(m2));
  }
    
  public MoneyOps scaleBy(double factor)
  {
    return new USMoney(numCents * factor / 100.0);
  }
}

The constructors each mention the fields that they initialize in their assignable clause. This is because the constructor's job is to initialize these fields. One can think of a new expression in Java as executing in two steps: allocating an object, and then calling the constructor. Thus the specification of a constructor needs to mention the fields that it can initialize in the assignable clause.

The first constructor's specification also illustrates that redundancy can also be used in an assignable clause. A redundant assignable clause follows if the meaning of the set of locations named is a subset of the ones denoted by the non-redundant clause for the same specification case. In this example the redundant assignable clause follows from the given assignable clause and the meaning of the depends clause inherited from the superclass MoneyAC.

The second constructor above is noteworthy in that there is a redundant ensures clauses that uses an informal predicate [Leavens96b]. In this instance, the informal predicate is used as a comment (which could also be used). Recall that informal predicates allow an escape from formality when one does not wish to give part of a specification in formal detail.

The plus and minus methods use assume statements; these are like assertions, but are intended to impose obligations on the callers [Back-Mikhajlova-vonWright98]. The main distinction between a assume statement and a requires clause is that the former is a statement and can be used within code. These may also be treated differently by different tools. For example, ESC/Java [Leino-etal00] will require callers to satisfy the requires clause of a method, but will not enforce the precondition if it is stated as an assumption.

2.4 Use of Pure Classes

Since USMoney is a pure class, it can be used to make models of other classes. An example is the abstract class specified in the file `Account.jml' below. The first model field in this class has the type USMoney, which was specified above. (Further explanation follows the specification below.)

package org.jmlspecs.samples.prelimdesign;

public class Account {

  //@ public model MoneyOps credit;
  //@ public model String owner;

  /*@ public invariant owner != null && credit != null
    @             && credit.greaterThanOrEqualTo(new USMoney(0));
    @*/
  //@ public constraint owner.equals(\old(owner));

  /*@  public normal_behavior
    @    requires own != null && amt != null
    @          && (new USMoney(1)).lessThanOrEqualTo(amt);
    @    assignable credit, owner;
    @    ensures credit.equals(amt) && owner.equals(own);
    @*/
  public Account(MoneyOps amt, String own);

  /*@  public normal_behavior
    @    assignable \nothing;
    @    ensures \result.equals(credit);
    @*/
  public pure MoneyOps balance();

  /*@  public normal_behavior
    @    requires 0.0 <= rate && rate <= 1.0
    @          && credit.can_scaleBy(1.0 + rate);
    @    assignable credit;
    @    ensures credit.equals(\old(credit.scaleBy(1.0 + rate)));
    @ for_example
    @  public normal_example
    @    requires rate == 0.05 && (new USMoney(4000)).equals(credit);
    @    assignable credit;
    @    ensures credit.equals(new USMoney(4200));
    @*/
  public void payInterest(double rate);

  /*@  public normal_behavior
    @    requires amt != null
    @           && amt.greaterThanOrEqualTo(new USMoney(0))
    @           && credit.can_add(amt);
    @    assignable credit;
    @    ensures credit.equals(\old(credit.plus(amt)));
    @ for_example
    @  public normal_example
    @    requires credit.equals(new USMoney(40000))
    @           && amt.equals(new USMoney(1));
    @    assignable credit;
    @    ensures credit.equals(new USMoney(40001));
    @*/
  public void deposit(MoneyOps amt);

  /*@  public normal_behavior
    @   requires amt != null && (new USMoney(0)).lessThanOrEqualTo(amt)
    @          && amt.lessThanOrEqualTo(credit);
    @    assignable credit;
    @    ensures credit.equals(\old(credit.minus(amt)));
    @ for_example
    @  public normal_example
    @    requires credit.equals(new USMoney(40001))
    @           && amt.equals(new USMoney(40000));
    @    assignable credit;
    @    ensures credit.equals(new USMoney(1));
    @*/
  public void withdraw(MoneyOps amt);
}

The specification of Account makes good use of examples. It also demonstrates the various ways of protecting predicates used in the specification from undefinedness [Leavens-Wing97a]. The principal concern here, as is often the case when using reference types in a model, is to protect against the model fields being null. As in Java, fields and variables of reference types can be null. In the specification of Account, the invariant states that these fields should not be null. Since implementations of public methods must preserve the invariants, one can think of the invariant as conjoined to the precondition and postcondition of each public method, and the postcondition of each public constructor. Hence, for example, method pre- and postconditions do not have to state that the fields are not null. However, often other parts of the specification must be written to allow the invariant to be preserved, or established by a constructor. For example, in the specification of Account's constructor, this is done by requiring amt and own are not null, since, if they could be null, then the invariant could not be established.

2.5 Composition for Container Classes

The following specifications lead to the specification of a class Digraph (directed graph). This gives a more interesting example of how more complex models can be composed in JML from other classes. In this example we use model classes and the pure containers provided in the package org.jmlspecs.models.

2.5.1 NodeType

The file `NodeType.java' contains the specification of an abstract class NodeType. NodeType is an abstract class, as opposed to a model class, because it will require an implementation and does appear in the interface of the model class Digraph. However, we also declare this abstract class to be pure, since we want to use its methods in the specification of other classes. (And we do so appropriately, since all the methods for class NodeType are side-effect-free.) In the abstract class specification for NodeType we simply provide a model field iD, which would represent a unique identifier for nodes.

package org.jmlspecs.samples.digraph;

import org.jmlspecs.models.*;

public /*@ pure @*/ abstract class NodeType implements JMLType {

  //@ public model int iD;

  /*@ also
    @   assignable \nothing;
    @ also
    @   public normal_behavior
    @    {|
    @       requires o instanceof NodeType;
    @       ensures \result == (iD == ((NodeType)o).iD);
    @     also
    @       requires !(o instanceof NodeType);
    @       ensures \result == false;
    @    |}
    @*/
  public abstract boolean equals(Object o);

  /*@ also
    @   public normal_behavior
    @     assignable \nothing;
    @     ensures \result instanceof NodeType
    @          && ((NodeType)\result).equals(this);
    @*/
  public abstract Object clone();

} // end of class NodeType

The use of also in the specification of NodeType's equals method is interesting. It separates two cases of the normal behavior for that method. This is equivalent to using two public normal_behavior clauses, one for each case. That is, when the argument is an instance of NodeType, the method must return true just when this and o have the same iD field. And when o is not an instance of NodeType, the equals method must return false. Compare this with the specification of the equals method for the class ArcType below (see section 2.5.2 ArcType).

2.5.2 ArcType

ArcType is specified as a pure model class in the file `ArcType.jml' shown below. It is a model class because it does not appear in the interface to Digraph, and so does not need to be implemented. We declare ArcType to be a pure class so that its methods can be used in assertions. The two model fields for ArcType, from and to, are both of type NodeType. We specify the equals method so that two references to objects of type ArcType are equal if and only if they have equal values in the from and to model fields. Thus, equals is specified using NodeType.equals. We also specify that ArcType has a public clone method, fulfilling the obligations of a type that implements JMLType. ArcType must implement JMLType so that its objects can be placed in a JMLValueSet. We use such a set for one of the model fields of Digraph.

package org.jmlspecs.samples.digraph;

import org.jmlspecs.models.JMLType;

public pure model class ArcType implements JMLType {

    public model NodeType from;
    public model NodeType to;
    public invariant from != null && to != null;

    public normal_behavior
      requires from != null && to != null;
      assignable this.from, this.to;
      ensures this.from.equals(from) && this.to.equals(to);
    public ArcType(NodeType from, NodeType to);

    also
      public normal_behavior
        requires o instanceof ArcType;
        ensures \result <==> ((ArcType)o).from.equals(from)
             && ((ArcType)o).to.equals(to);
    also
      public normal_behavior
        requires !(o instanceof ArcType);
        ensures \result == false;
    public boolean equals(Object o);

    also
      public normal_behavior
        ensures \result instanceof ArcType
             && ((ArcType)\result).equals(this);
    public Object clone();
}

2.5.3 Digraph

Finally, the specification of the class Digraph is given in the file `Digraph.jml' shown below. This specification demonstrates how to use container classes, like JMLValueSet, combined with appropriate invariants to specify models that are compositions of other classes. Both the model fields nodes and arcs are of type JMLValueSet. However, the first invariant clause restricts nodes so that every object in nodes is, in fact, of type NodeType. Similarly, the next invariant clause we restrict arcs to be a set of ArcType objects. In both cases, since the type is JMLValueSet, membership is determined by the equals method for the type of the elements (rather than reference equality).

package org.jmlspecs.samples.digraph;
//@ model import org.jmlspecs.models.*;
public class Digraph {

 //@ public model JMLValueSet nodes;
 //@ public model JMLValueSet arcs;

 /*@ public invariant nodes != null
   @   && (\forall JMLType n; nodes.has(n); n instanceof NodeType);
   @ public invariant arcs != null
   @   && (\forall JMLType a; arcs.has(a); a instanceof ArcType); 
   @ public invariant (\forall ArcType a; arcs.has(a);
   @                       nodes.has(a.from) && nodes.has(a.to));
   @*/

 /*@  public normal_behavior
   @   assignable nodes, arcs;
   @   ensures nodes.isEmpty() && arcs.isEmpty();
   @*/
 public Digraph();

 /*@  public normal_behavior
   @   requires n != null;
   @   assignable nodes;
   @   ensures nodes.equals(\old(nodes.insert(n)));
   @*/
 public void addNode(NodeType n);
 
 /*@  public normal_behavior
   @   requires unconnected(n);
   @   assignable nodes;
   @   ensures nodes.equals(\old(nodes.remove(n)));
   @*/
 public void removeNode(NodeType n);
 
 /*@  public normal_behavior
   @   requires inFrom != null && inTo != null
   @         && nodes.has(inFrom) && nodes.has(inTo);
   @   assignable arcs;
   @   ensures arcs.equals(
   @              \old(arcs.insert(new ArcType(inFrom, inTo))));
   @*/
 public void addArc(NodeType inFrom, NodeType inTo);

 /*@  public normal_behavior
   @   assignable \nothing;
   @   ensures \result == nodes.has(n);
   @*/
 public pure boolean isNode(NodeType n); 

 /*@  public normal_behavior
   @   ensures \result == arcs.has(new ArcType(inFrom, inTo));
   @
   @*/
 public pure boolean isArc(NodeType inFrom, NodeType inTo); 

 /*@  public normal_behavior
   @   requires nodes.has(start) && nodes.has(end);
   @   assignable \nothing;
   @   ensures \result == reachSet(new JMLValueSet(start)).has(end);
   @*/
 public pure boolean isAPath(NodeType start, NodeType end);

 /*@  public normal_behavior
   @   assignable \nothing;
   @   ensures \result <==>
   @              !(\exists ArcType a; arcs.has(a);
   @                     a.from.equals(n) || a.to.equals(n));
   @ public pure model boolean unconnected(NodeType n);
   @*/

 /*@  public normal_behavior
   @   requires nodeSet != null
   @    && (\forall JMLType o; nodeSet.has(o);
   @         o instanceof NodeType && nodes.has(o));
   @   {|
   @      measured_by nodes.size() - nodeSet.size();
   @      assignable \nothing;
   @    also
   @      requires nodeSet.equals(OneMoreStep(nodeSet));
   @      ensures \result != null && \result.equals(nodeSet);
   @    also
   @      requires !nodeSet.equals(OneMoreStep(nodeSet));
   @      ensures \result != null
   @               && \result.equals(reachSet(OneMoreStep(nodeSet)));
   @   |}
   @ public pure model JMLValueSet reachSet(JMLValueSet nodeSet);
   @*/

 /*@  public normal_behavior
   @   requires nodeSet != null
   @    && (\forall JMLType o; nodeSet.has(o);
   @         o instanceof NodeType && nodes.has(o));
   @      assignable \nothing;
   @   ensures \result != null
   @    && \result.equals(nodeSet.union(
   @        new JMLValueSet { NodeType n | nodes.has(n)
   @          && (\exists ArcType a; a != null && arcs.has(a);
   @                    nodeSet.has(a.from) && n.equals(a.to))}));
   @ public pure model JMLValueSet OneMoreStep(JMLValueSet nodeSet);
   @*/
}  // end of class Digraph

An interesting use of pure model methods appears at the end of the specification of Digraph in the pure model method reachSet. This method constructively defines the set of all nodes that are reachable from the nodes in the argument nodeSet. This specification uses a nested case analysis, between {| and |}. The meaning of this is again that each pre- and postcondition pair has to be obeyed, but by using nesting, one can avoid duplication of the requires clause that is found at the beginning of the specification. The measured_by clause is needed because this specification is recursive; the measure given allows one to describe a termination argument, and thus ensure that the specification is well-defined. This clause defines an integer-valued measure that must always be at least zero; furthermore, the measure for a call and recursive uses in the specification must strictly decrease [Owre-etal95]. The recursion in the specification builds up the entire set of reachable nodes by, for each recursive reference, adding the nodes that can be reached directly (via a single arc) from the nodes in nodeSet.

2.6 Subtyping

Following Dhara and Leavens [Dhara-Leavens96] [Leavens97c], a subtype inherits the specifications of its supertype's public and protected members (fields and methods), as well as its public and protected invariants and history constraints.(26) This ensures that a subclass specifies a behavioral subtype of its supertypes. This inheritance can be thought of textually, by copying the public and protected specifications of the methods of a class's ancestors and all interfaces that a class implements into the class's specification and combining the specifications using also [Raghavan-Leavens00].(27) (This is the reason for the use of also at the beginning of specifications in overriding methods.) By the semantics of method combination using also, these behaviors must all be satisfied by the method, in addition to any explicitly specified behaviors.

For example, consider the class PlusAccount, specified in file `PlusAccount.jml' shown below. It is specified as a subclass of Account (see section 2.4 Use of Pure Classes). Thus it inherits the fields of Account, and Account's public invariants, history constraints, and method specifications. (The specification of Account given above does not have any protected specification information.) Because it inherits the fields of its superclass, inherited method specifications of behavior are still meaningful when copied to the subclass. The trick is to always add new model fields to the subclass and relate them to the existing ones.

Note that in the represents clause below, instead of a left-facing arrow, <-, the connective "\such_that" is used to introduce a relationship predicate. This form of the represents clause allows one to specify abstraction relations, instead of abstraction functions.

package org.jmlspecs.samples.prelimdesign;

public class PlusAccount extends Account {
  //@ public model MoneyOps savings, checking;

  //@ public depends credit <- savings, checking;
  /*@ public represents credit \such_that
    @                       credit.equals(savings.plus(checking));
    @*/
  //@ public invariant savings != null && checking != null;
  /*@ public invariant_redundantly savings.plus(checking)
    @                          .greaterThanOrEqualTo(new USMoney(0));
    @*/

  /*@  public normal_behavior
    @    requires sav != null && chk != null && own != null
    @          && (new USMoney(1)).lessThanOrEqualTo(sav)
    @          && (new USMoney(1)).lessThanOrEqualTo(chk);
    @    assignable credit, owner;
    @    assignable_redundantly savings, checking;
    @    ensures savings.equals(sav) && checking.equals(chk)
    @             && owner.equals(own);
    @    ensures_redundantly credit.equals(sav.plus(chk));
    @*/
  public PlusAccount(MoneyOps sav, MoneyOps chk, String own);

  /*@ also
    @  public normal_behavior
    @    requires 0.0 <= rate && rate <= 1.0
    @          && credit.can_scaleBy(1.0 + rate);
    @    assignable credit, savings, checking;
    @    ensures checking.equals(\old(checking.scaleBy(1.0 + rate)));
    @ for_example
    @  public normal_example
    @    requires rate == 0.05 && checking.equals(new USMoney(2000));
    @    assignable credit, savings, checking;
    @    ensures checking.equals(new USMoney(2100));
    @*/
  public void payInterest(double rate);

  /*@ also
    @  public normal_behavior
    @    requires amt != null
    @            && (new USMoney(0)).lessThanOrEqualTo(amt)
    @            && amt.lessThanOrEqualTo(savings);
    @    assignable credit, savings;
    @    ensures savings.equals(\old(savings.minus(amt)))
    @            && \not_modified(checking);
    @ also
    @  public normal_behavior
    @    requires amt != null
    @            && (new USMoney(0)).lessThanOrEqualTo(amt)
    @            && amt.lessThanOrEqualTo(credit)
    @            && amt.greaterThan(savings);
    @    assignable credit, savings, checking;
    @    ensures savings.equals(new USMoney(0))
    @           && checking.equals(
    @                    \old(checking.minus(amt.minus(savings))));
    @ for_example
    @   public normal_example
    @    requires savings.equals(new USMoney(40001))
    @             && amt.equals(new USMoney(40000));
    @    assignable credit, savings, checking;
    @    ensures savings.equals(new USMoney(1))
    @            && \not_modified(checking);
    @  also
    @   public normal_example
    @    requires savings.equals(new USMoney(30001))
    @           && checking.equals(new USMoney(10000))
    @           && amt.equals(new USMoney(40000));
    @    assignable credit, savings, checking;
    @    ensures savings.equals(new USMoney(0))
    @           && checking.equals(new USMoney(1));
    @*/
  public void withdraw(MoneyOps amt);

  /*@ also
    @  public normal_behavior
    @    requires amt != null
    @           && amt.greaterThanOrEqualTo(new USMoney(0))
    @           && credit.can_add(amt);
    @    assignable credit, savings;
    @    ensures savings.equals(\old(savings.plus(amt)))
    @            && \not_modified(checking);
    @ for_example
    @  public normal_example
    @    requires savings.equals(new USMoney(20000))
    @           && amt.equals(new USMoney(1));
    @    assignable credit, savings, checking;
    @    ensures savings.equals(new USMoney(20001));
    @*/ 
  public void deposit(MoneyOps amt);

  /*@    public normal_behavior
    @    requires amt != null
    @           && amt.greaterThanOrEqualTo(new USMoney(0))
    @           && credit.can_add(amt);
    @    assignable credit, checking;
    @    ensures checking.equals(\old(checking.plus(amt)))
    @          && \not_modified(savings);
    @ for_example
    @  public normal_example
    @    requires checking.equals(new USMoney(20000))
    @           && amt.equals(new USMoney(1));
    @    assignable credit, checking;
    @    ensures checking.equals(new USMoney(20001));
    @*/
  public void depositToChecking(MoneyOps amt);

  /*@  public normal_behavior
    @    requires amt != null;
    @    {|
    @      requires (new USMoney(0)).lessThanOrEqualTo(amt)
    @             && amt.lessThanOrEqualTo(checking);
    @      assignable credit, checking;
    @      ensures checking.equals(\old(checking.minus(amt)))
    @             && \not_modified(savings);
    @     also
    @      requires (new USMoney(0)).lessThanOrEqualTo(amt)
    @             && amt.lessThanOrEqualTo(credit)
    @             && amt.greaterThan(checking);
    @      assignable credit, checking, savings;
    @      ensures checking.equals(new USMoney(0))
    @          && savings.equals(
    @                   \old(savings.minus(amt.minus(checking))));
    @    |}
    @ for_example
    @  public normal_example 
    @    requires checking.equals(new USMoney(40001))
    @           && amt.equals(new USMoney(40000));
    @    assignable credit, checking;
    @    ensures checking.equals(new USMoney(1))
    @           && \not_modified(savings);
    @ also
    @  public normal_example
    @    requires savings.equals(new USMoney(30001))
    @           && checking.equals(new USMoney(10000))
    @           && amt.equals(new USMoney(40000));
    @    assignable credit, checking, savings;
    @    ensures checking.equals(new USMoney(0))
    @          && savings.equals(new USMoney(1));
    @*/
  public void payCheck(MoneyOps amt);
}


Go to the first, previous, next, last section, table of contents.