[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

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  
2.2 Data Groups  
2.3 Types For Modeling  
2.4 Use of Pure Classes  
2.5 Composition for Container Classes  
2.6 Behavioral Subtyping  


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;
    @ public 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  
2.1.2 Invariants  
2.1.3 Method Specifications  
2.1.4 Models and Lightweight Specifications  


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 is not part of the Java implementation, and must appear in an annotation; however, for purposes of the specification we treat it 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 is not part of the Java implementation, since it is modified by the keyword model. Such model imports must also appear in annotation comments. In general, any declaration form in Java can have the model 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 be true of the field's starting value. That is, all reachable objects of the type UnboundedStack must 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.(9) 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  
2.1.3.2 Old Values  
2.1.3.3 Reference Semantics  
2.1.3.4 Correct Implementation  


2.1.3.1 The Assignable Clause

The use of the assignable(10) 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 in theStack's data group). This allows push to assign to theStack (and the members of its data group), 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,(11) 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.(12) 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 the locations corresponding to formal parameters in the assignable clause. However, the locations corresponding to fields or array elements of such formal parameters can be sensibly mentioned 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 to 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 locations of their data group members) 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 "location" for a model field or model variable cannot be directly assigned to in JML, its value is determined by the concrete fields and variables that it (ultimately) depends on, specifically the members of its data group. That is, a model field or variable can be modified by assignments to the concrete members of its data group (see section 2.2 Data Groups). Thus, a method's assignable clause only permits the method to modify a location if the location:

In the specification of top, the assignable clause says that a call to top that satisfies 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, the default store-ref for the assignable clause is \everything. Thus an omitted assignable clause in JML means that the method can assign to all locations (that could otherwise be assigned to by the method). 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.


2.1.3.3 Reference Semantics

Note also that, since JMLObjectSequence is a reference type, one must use equals instead of == to compare instances of this type for equality of values. For example, in the postcondition of the pop method, we use equals to compare theStack and \old(theStack.trailer()), as these may yield different objects. Using == would be a mistake, since it would only compare them for object identity.

As in Java itself, most types are reference types, and hence many expressions yield references (i.e., object identities or addresses), as opposed to primitive values. This means that ==, except when used to compare pure values of primitive types such as boolean or int, is reference equality. As in Java, to get value equality for reference types one uses the equals method in assertions. For example, the predicate myString == yourString, is only true if the objects denoted by myString and yourString are the same object (i.e., if the names are aliases); to compare their values one must write myString.equals(yourString).


2.1.3.4 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.1.4 Models and Lightweight Specifications

In specifying existing code, one often does not want to introduce new model fields or think up new names for them. And sometimes, especially for fields with simple, atomic values, the field name itself is so "natural" that it would be difficult to think up a second good name for a model field that would be an abstraction of it. Thus JML provides two modifiers, spec_public and spec_protected that can used to make existing fields public or protected, for purposes of specification.

For example, consider the (lightweight) specification of the class Point2D below. In this specification the private fields, x and y are specified as spec_public, which allows them to be used in the public invariant clause and in the (implicitly public) specifications of the constructors and methods of Point2D.

 
package org.jmlspecs.samples.prelimdesign;

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

public class Point2D
{
  private /*@ spec_public @*/ double x = 0.0;
  private /*@ spec_public @*/ double y = 0.0;

  //@ public invariant !Double.isNaN(x);
  //@ public invariant !Double.isNaN(y);
  //@ public invariant !Double.isInfinite(x);
  //@ public invariant !Double.isInfinite(y);

  //@ ensures x == 0.0 && y == 0.0;
  public Point2D() { }

  /*@ requires !Double.isNaN(xc);
    @ requires !Double.isNaN(yc);
    @ requires !Double.isInfinite(xc);
    @ requires !Double.isInfinite(yc);
    @ assignable x, y;
    @ ensures x == xc && y == yc;
    @*/
  public Point2D(double xc, double yc) {
    x = xc;
    y = yc;
  }

  //@ ensures \result == x;
  public /*@ pure @*/ double getX() {
    return x;
  }

  //@ ensures \result == y;
  public /*@ pure @*/ double getY() {
    return y;
  }
  
  /*@ requires !Double.isNaN(x+dx);
    @ requires !Double.isInfinite(x+dx);
    @ assignable x;
    @ ensures JMLDouble.approximatelyEqualTo(x,
    @                       \old(x+dx), 1e-10);
    @*/
  public void moveX(double dx) {
    x += dx;
  }
  
  /*@ requires !Double.isNaN(y+dy);
    @ requires !Double.isInfinite(y+dy);
    @ assignable y;
    @ ensures JMLDouble.approximatelyEqualTo(y,
    @                       \old(y+dy), 1e-10);
    @*/
  public void moveY(double dy) {
    y += dy;
  }
}

Note that these specifications would be illegal without the use of spec_public, since JML requires that public specifications only mention publicly-visible names (see section 1.1 Behavioral Interface Specification).

However, spec_public is more than just a way to change the visibility of a name for specification purposes. When applied to fields it can be considered to be shorthand for the declaration of a model field with the same name. That is, the declaration of x in Point2D can be thought of as equivalent to the following declarations, together with a rewrite of the Java code that uses x to use _x instead (where we assume _x is not used elsewhere).

 
  //@ public model int x;
  private int _x; //@ in x;
  //@ private represents x <- _x;

So in this way of thinking spec_public is not just an access modifier, but shorthand for declaration of a model field. This model field declaration is a commitment to readers that they can understand the specification using these model fields, even if the underlying private fields are changed, just as if the model field were declared explicitly. The model fields that are implicit allow such changes to be made without affecting the readers of the specification.

For example, suppose one wanted to change the implementation of Point2D, to use polar coordinates. To do that while keeping the public specification unchanged, one would declare the model fields x and y explicitly. One would then declare other fields for the polar and rectangular coordinates (and perhaps additional model fields as well). One would then also need to give explicit declarations that the new concrete fields are members of the model fields data groups, and give appropriate represents clauses. (See section 2.2.2.1 Data Groups and Represents Clauses, for more on data group membership and represents clauses.) All of this is exactly analogous to what is done implicitly in the the desugaring described above.

Similar remarks apply to spec_protected. The spec_public and spec_protected shorthands were borrowed from ESC/Java, but the desugaring described above is novel with JML.


2.2 Data Groups

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  
2.2.2 Specification of BoundedStackInterface  


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_only CloneNotSupportedException;
      @*/
    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  
2.2.1.2 Invariants and History Constraint  
2.2.1.3 Details of the Method Specifications  
2.2.1.4 Adding to Method Specifications  
2.2.1.5 Specifying Exceptional Behavior  


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.(13)

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 Invariants 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,(14) 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-Leavens05].

 
     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 a method may not return normally. 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-Leavens05].

 
     ensures false;

This formalizes the idea that a method with an exceptional_behavior specification may not return normally when the specification's precondition is satisfied. Thus, when the precondition of such a specification case holds, some exception must be thrown (unless the execution encounters an error or is permitted to not return to the caller).

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.

The specification of clone also illustrates the signals_only clause. The signals_only clause in the example says that the method may only throw an exception that is a subtype of CloneNotSupportedException when the exceptional behavior's precondition is true. This says the same thing as the following, more verbose, signals clause.

 
     signals (Exception e) e instanceof CloneNotSupportedException;

The signals clause itself only describes what must be true when the exceptions it applies to are thrown; it does not constrain a method's behavior with respect to exceptions that are not subtypes of the exceptions named. For example, a signals clause of the form

 
    signals (CloneNotSupportedException) true;

would only say that a CloneNotSupportedException can always be thrown; it would not prohibit other exceptions that are not subtypes of CloneNotSupportedException from being thrown. For example, if clone were specified with such a signals clause, then an implementation could legally throw a NullPointerException. To prevent such a possibility, in many cases it is preferable to use a signals_only clause to limit what exceptions may be thrown.

Finally note that in the specification of clone, the normal 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 initially theStack != null && theStack.isEmpty();
  /*@ public model instance JMLObjectSequence theStack;
    @                                             in size;
    @*/
  //@ public instance represents size <- theStack.int_length();
  /*@ public instance invariant theStack != null;
    @ public instance invariant_redundantly
    @                           theStack.int_length() <= MAX_SIZE;
    @ public instance invariant 
    @         (\forall int i; 0 <= i && i < theStack.int_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_only BoundedStackException;
    @*/
  public void pop( ) throws BoundedStackException;

  /*@   public normal_behavior
    @     requires theStack.int_length() < MAX_SIZE && x != null;
    @     assignable size, theStack;
    @     ensures theStack.equals(\old(theStack.insertFront(x)));
    @     ensures_redundantly theStack != null && top() == x
    @              && theStack.int_length() 
    @                     == \old(theStack.int_length()+1);
    @ also
    @   public exceptional_behavior
    @     requires theStack.int_length() >= MAX_SIZE || x == null;
    @     assignable \nothing;
    @     signals_only BoundedStackException, NullPointerException;
    @     signals (BoundedStackException)
    @                  theStack.int_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_only BoundedStackException;
    @     signals (BoundedStackException e)
    @             \fresh(e) && e != null && e.getMessage() != null
    @           && e.getMessage().equals("empty stack");
    @*/
  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 Data Groups and Represents Clauses  
2.2.2.2 Redundant Specification  
2.2.2.3 Multiple Specification Cases  
2.2.2.4 Pitfalls in Specifying Exceptions  
2.2.2.5 Redundant Ensures Clauses  


2.2.2.1 Data Groups and Represents Clauses

The in and represents clauses that follow the declaration of theStack are an important feature in modeling with layers of model fields.(15) 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.

When a model field is declared, a data group with the same name is automatically created; furthermore, this field is always a member of the group it creates. A data group is a set of fields (locations) referenced by a specific name, i.e., the name of the model field that created it [Leino98] [Leino-Poetzsch-Heffter-Zhou02].

When a data group (or field) is mentioned in the assignable clause for a method M, then all members (i.e., fields) in that group can be assigned to in the body of M. Fields can become a member of a data group through the data group clauses (i.e., the in and maps-into clauses) that come immediately after the field declaration, in this case the in clause. The in clause in BoundedStackInterface says that theStack is a member of the group created by the declaration of model field size; this means that theStack might change its value whenever size changes. However, 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 member of size.

The maps-into clause is another way of adding members to a data group; it allows the fields of an object to be included in an existing data group. For example, if a field F is a reference or an array type, then the fields or array elements of F can be included in a data group using the maps-into clause. The following are examples.
 
  protected ArrayList elems;
  //@             maps elems.theList \into theStack;
  protected java.lang.Object[] theItems;
  //@             maps theItems[*] \into theStack;

In the first example, the maps-into clause says that theList field of elems is a member of theStack data group. Field elems is a concrete field of the type (i.e., it is not a model field and thus is part of the implementation). This allows model field theList of elems to change when theStack changes. Since theList is a model field and data group, this also allows concrete fields of elems to change as theStack changes. Similarly, the second example says that the elements of the array, theItems, can change when theStack changes.

Data groups have the same visibility as the model field that declared it, i.e, public, protected, private, or package visibility. A field cannot be a member of a group that is less visible than it is. For example, a public field cannot be a member of a protected group.

The in and maps-into clauses are 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 are members of other groups. For example, since theStack is a member of size, whenever size is mentioned in an assignable clause, then theStack is implicitly allowed to be modified.(16) 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 size is not a member of theStack's group. Furthermore, it is redundant to mention theStack when size has already been mentioned (although this can help clarify the assignable clause, i.e., clarify which fields can be changed).

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 data group members. To state relationships among concrete data fields or on fields that are not related by a data group membership, 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

After 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-Leavens05] 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 default signals clause has been added. This clause was omitted from the original specification, since no particular details of the exception object were important to the specifier.

 
//@ 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_only BoundedStackException;
    @     signals (java.lang.Exception) 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. To compensate for this, the predicate \not_assigned, is used in the exceptional behavior specification cases to prohibit assignment to the locations (those in the data groups of size and theStack) that are now part of the assignable clause. 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, theStack;
    @     ensures \old(!theStack.isEmpty())
    @               ==> theStack.equals(\old(theStack.trailer()));
    @     ensures \old(theStack.isEmpty()) ==> 
    @                 \not_assigned(size) && \not_assigned(theStack);
    @     signals_only BoundedStackException;
    @     signals (java.lang.Exception)
    @              \old(!theStack.isEmpty()) ==> false;
    @     signals (java.lang.Exception)
    @              \old(theStack.isEmpty()) ==>
    @               \not_assigned(size) && \not_assigned(theStack)
    @               && 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 different signals clauses may both apply 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.(17) The problem is that both exceptional preconditions may be true, and in that case an implementation cannot throw an exception that is an instance of both a BoundedStackException and a NullPointerException.

 
  /*@   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 (Exception e) e instanceof BoundedStackException;
    @ also                                   // this is wrong!
    @   public exceptional_behavior
    @     requires x == null;
    @     assignable \nothing;
    @     signals (Exception e) e instanceof 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 signals clauses that do not exclude other exceptions from being thrown whenever there are states in which multiple exceptions may be thrown. That is, instead of using multiple signals_only clauses or using multiple signals clauses like:
 
   signals (Exception e) e instanceof BoundedStackException;
which only allows a BoundedStackException to be thrown when the precondition is true, one can write a signals clause like:
 
   signals (BoundedStackException);
which says nothing about what happens when other exceptions are thrown (see section 2.2.1.5 Specifying Exceptional Behavior for more details).


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.(18)

In summary, using types like JMLObjectSequence for modeling can help the specifier give more precise specifications. We describe more about such types in the next section.


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  
2.3.2 Money  
2.3.3 MoneyComparable and MoneyOps  
2.3.4 MoneyAC  
2.3.5 MoneyComparableAC  
2.3.6 USMoney  


2.3.1 Purity

We say a method is pure if it is either specified with the modifier pure or is a 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 has the clauses
 
           diverges false;
           assignable \nothing;
added to each specification case; if the method has no specification given explicitly, then these clauses are added as a lightweight specification. For this reason, if one is writing a pure method, it is not necessary to otherwise specify an assignable clause (see section 2.1.3.1 The Assignable Clause), although doing so may improve the specification's clarity.

A pure constructor has the clauses
 
           diverges false;
           assignable this.*;
added to each specification case; if the constructor has no specification given explicitly, then these clauses are added as a lightweight specification. This specification allows the constructor to assign to the non-static fields of the class in which it appears (including those inherited from its superclasses and model and ghost instance fields from the interfaces that it implements).

Implementations of pure methods and constructors will be checked to see that they meet these conditions; i.e., that pure methods do not assign to locations that exist in the pre-state, and that pure constructors only assign to pre-existing locations that are fields of the this object. To make such checking modular, some JML tools prohibit a pure method or constructor implementation from calling methods or constructors that are not pure. However, more sophisticated tools could more directly check the intended semantics [Salcianu-Rinard05].

A pure method or constructor must also be provably terminating. Although JML does not force users to make such proofs of termination, users writing pure methods and constructors are supposed to make pure methods total in the sense that whenever, a pure method is called it either returns normally or throws some exception. This is supposed to lessen the possibility that assertion evaluation could loop forever, help make pure methods more like mathematical functions, and help the runtime assertion checker. The runtime assertion checker turns exceptions into arbitrary values of the appropriate result type [Cheon03] [Cheon-Leavens05]; it cannot do anything with infinite loops.

Furthermore, a pure method is supposed to always either terminate normally or throw an exception, even for calls that do not satisfy its precondition. Static verification tools for JML should enforce this condition, by requiring a proof that a pure method implementation satisfies the following specification
 
   private behavior
     requires true;
     diverges false;
     assignable \nothing;
(and similarly for constructors, except that the assignable clause becomes assignable this.*; for constructors).

However, this implicit verification condition is a specification, and is thus cannot be used in reasoning about calls to the method, even calls from within the class itself and recursive calls from within the implementation. For this reason we recommend writing the method or constructor specification in such a way that the effective precondition of the method is "true," making the proof of the above implicit verification condition trivial, and allowing the termination behavior of the implementation to be relied upon by all clients.

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.

Furthermore, a pure method must be deterministic, in the sense that when called in a given state, it must always return the same value. Similarly a pure constructor should be deterministic in the sense that when called in a given state, it always initializes the object in the same way.

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. 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); conversely, a Java method can be pure (and thus 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(/*@ nullable @*/ 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.(19)

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

2.3.2.1 Redundant Examples  
2.3.2.2 JMLType and Informal Predicates  


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(20) 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.20 $
 * @author Gary T. Leavens and Albert L. Baker.
 * @see JMLObjectType
 * @see JMLValueType
 */
//@ pure
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(/*@ nullable @*/ 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.(21)

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.


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
    @     old boolean can_add = can_add(m2); // FIXME: inline.
    @     requires m2 != null && can_add;
    @     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
    @     old boolean inRange = inRange((double) pennies - m2.pennies); // FIXME: inline.
    @     requires m2 != null
    @           && inRange;
    @     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 in, maps-into, 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.(22) 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;
  //@                in pennies;

  //@ 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(/*@ nullable @*/ Object o2) {
    if (o2 instanceof Money) {
      Money m2 = (Money)o2;
      return numCents
             == (100 * m2.dollars() + m2.cents());
    } else {
      return false;
    }
  }

  public int hashCode() {
    return (int)numCents;
  }

  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 /*@ pure @*/
  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.(23)

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)
  {
    return new USMoney(numCents + totalCents(m2));
  }

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

  public String toString()
  {
    return "$" + dollars() + "." + cents();
  }
}

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 in clause inherited from the superclass MoneyAC.

The second constructor above is noteworthy in that there is a redundant ensures clause 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 accountOwner;
  /*@ public invariant accountOwner != null && credit != null
    @         && credit.greaterThanOrEqualTo(new USMoney(0)); @*/
  //@ public constraint accountOwner.equals(\old(accountOwner));

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

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

  /*@  public normal_behavior
    @    old boolean can_scale = credit.can_scaleBy(1.0 + rate);
    @    requires 0.0 <= rate && rate <= 1.0
    @          && can_scale;
    @    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
    @    old boolean can_add = credit.can_add(amt);
    @    requires amt != null
    @          && amt.greaterThanOrEqualTo(new USMoney(0))
    @          && can_add;
    @    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 and the postcondition 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  
2.5.2 ArcType  
2.5.3 Digraph  


2.5.1 NodeType

The file `NodeType.java' contains the specification of an interface NodeType. We also declare this interface to be pure, since we want to use its methods in the specifications of other classes. (This is appropriate, since all the methods of NodeType are side-effect free.)

 
package org.jmlspecs.samples.digraph;

import org.jmlspecs.models.*;

public /*@ pure @*/ interface NodeType extends JMLType {
  
  /*@ also
    @   public normal_behavior
    @       requires !(o instanceof NodeType);
    @       ensures \result == false;
    @*/
  public boolean equals(/*@ nullable @*/ Object o);

  public int hashCode();

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

}


2.5.2 ArcType

ArcType is specified as a pure class in the file `ArcType.jml' shown below. In theory, this class could have been declared with the model modifier, since it does not appear in the interface to Digraph. However, we specify it as a normal Java class for simplicity, and because model classes do not currently work in JML's runtime assertion checker. 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;

/*@ pure @*/ public 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
      @     requires !(o instanceof ArcType);
      @     ensures \result == false;
      @   |}
      @*/
    public boolean equals(/*@ nullable @*/ Object o);

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

The use of also in the specification of ArcType'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 ArcType, the method must return true just when this and o have the same from and to fields. And when o is not an instance of ArcType, the equals method must return false.


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. In this specification, the container class JMLValueSet is used as the type of the model fields nodes and arcs. Since JML currently only works with a non-generic version of Java, 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_redundantly nodes != null;
   @ public invariant (\forall JMLType n; nodes.has(n);
   @                          n instanceof NodeType);
   @ public invariant_redundantly arcs != null;
   @ public invariant (\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_redundantly 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_redundantly inFrom != null && inTo != null;
   @   requires 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
   @   requires_redundantly inFrom != null && inTo != null;
   @   requires nodes.has(inFrom) && nodes.has(inTo);
   @   assignable arcs;
   @   ensures arcs.equals(
   @            \old(arcs).remove(new ArcType(inFrom, inTo)));
   @*/
 public void removeArc(NodeType inFrom, NodeType inTo);

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

 /*@  public normal_behavior
   @   requires_redundantly inFrom != null && inTo != null;
   @   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 @*/ boolean unconnected(NodeType n);

 /*@  public normal_behavior
   @   requires_redundantly nodeSet != null;
   @   requires (\forall JMLType o; nodeSet.has(o);
   @                o instanceof NodeType && nodes.has(o));
   @   {|
   @      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_redundantly nodeSet != null;
   @   requires (\forall JMLType o; nodeSet.has(o);
   @              o instanceof NodeType && nodes.has(o));
   @      assignable \nothing;
   @   ensures_redundantly \result != null;
   @   ensures \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);
   @*/
}

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 Behavioral Subtyping

As in Java, a subtype inherits members (fields and methods) from its supertypes. A subtype also inherits all the class level-specifications associated with fields and all method specifications for public and protected instance methods. This specification inheritance has the effect of making the subtype a behavioral subtype [Liskov-Wing94], in the sense that instances of the subtype obey the specifications its supertype(s) [Dhara-Leavens96] [Leavens-Weihl95].

Class-level specifications associated with fields include include invariants and history constraints (see section 2.2.1.2 Invariants and History Constraint), as well as initially clauses (see section 2.1.1 Model Fields) data group declarations (see section 2.2 Data Groups), and represents clauses (see section 2.2.2.1 Data Groups and Represents Clauses). Inheritance of invariants means that each supertype's invariants must also hold in the subtype. Similarly, every history constraint specified in each supertype must be obeyed in the subtype. And all initially clauses specified for supertype fields must also be obeyed in all subtypes. Fields declared in a supertype retain their data group membership when inherited. Their represents clauses are also inherited.

As in Java, private fields are inherited by a subtype but not visible to it. Similarly, default privacy (i.e., package visibility) fields are not accessible if the subtype is declared in a different package than the supertype declaring the field. As in Java, these fields are present in the objects of the subtype, but not accessible to code written in the subtype. In the same way, class level specifications associated with such fields must still be obeyed by objects of the subtype. Various restrictions to JML that ensure that this is always possible are being investigated [Ruby-Leavens00].

Specifications for instance methods are also inherited in the sense that public and protected specification cases must be obeyed by all overriding methods [Dhara-Leavens96] [Leavens97c]. This inheritance of method specifications ensures that a client's reasoning about a method call will still be valid, even if the method is overridden [America87] [America91] [Leavens-Weihl95], and thus that a subclass is a behavioral subtype of its supertypes [Dhara-Leavens96]. Note that private and default (package) visibility specification cases are not visible to subtypes, and hence do not have to be obeyed by them; not inheriting such specification cases does not cause clients reasoning problems, as these specification cases are not visible to clients making method calls (in general).(24) Furthermore, specifications are not inherited for constructors or for static methods, since they are not involved in dynamic dispatch.

Inheritance of method specifications can be thought of textually. For each instance method, m specified in a class C, one can imagine copying into the specification of m the public and protected specification cases for m given in all of C's ancestors and in all the interfaces C implements; these specification cases would be combined using also [Dhara-Leavens96] [Raghavan-Leavens05].(25) (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.) Since it inherits the fields of its superclass, a textual copy of the method specification cases of Account would still be meaningful in the context of PlusAccount. Thinking of such textual copies works if one adds new (model) fields to specify the subclass and relates them to the existing ones. If instead one tried to respecify the fields of a supertype with invariants and history constraints that violated the (inherited) specification of that supertype, then the resulting specification would be contradictory, and hence not be correctly implementable.

 
package org.jmlspecs.samples.prelimdesign;

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

  /*@ 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
    @    old boolean can_scale = credit.can_scaleBy(1.0 + rate);
    @    requires 0.0 <= rate && rate <= 1.0
    @          && can_scale;
    @    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
    @    old boolean can_add = credit.can_add(amt);
    @    requires amt != null
    @           && amt.greaterThanOrEqualTo(new USMoney(0))
    @           && can_add;
    @    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
    @    old boolean can_add = credit.can_add(amt);
    @    requires amt != null
    @           && amt.greaterThanOrEqualTo(new USMoney(0))
    @           && can_add;
    @    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);
}

Similarly, if one tried to respecify a method in a way that violated an (inherited) specification case, then the method would have to obey both specifications, and would not be correctly implementable. Thus, specification inheritance guarantees that all subtypes are behavioral subtypes in JML, and trying to avoid behavioral subtyping results in unimplementable specifications Dhara-Leavens96.

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.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Gary Leavens on March, 16 2009 using texi2html