We have introduced a few kinds of method specification clauses so far. In fact there are many more, though most are not widely used:

Some of these have been already discussed; others are discussed in later lessons; and others are omitted from the tutorial because they are too advanced or too ill-defined – see the JML Reference Manual for details on those. The old clause is presented below. Clauses discussed in this tutorial are clickable hyperlinks in the above list.

Ordering of clauses

There is no pre-defined order to the clauses within a single specification case (the same applies to multiple specification cases). However, a specification is more readable (by people familiar with JML) if the clauses generally follow the order above, with preconditions first, then frame conditions, followed by postconditions.

There is some meaning to the ordering within the precondition group and within the postcondition group: earlier clauses can enforce conditions that are needed for later clauses to be well-defined; but ordering only matters within the each kinds of clause; that is, ordering matters within the precondition clauses and separately within the postcondition clauses (ensures clauses). For example, when the following is checked with ESC

// openjml --esc T_order1.java
//@ nullable_by_default // for the purpose of this example
public class T_order1 {

  //@ requires a.length > 10;  // ERROR: a might be null!
  //@ requires a != null;
  public void m(int[] a) {}

}

the output is as follows.

T_order1.java:5: verify: The prover cannot establish an assertion (UndefinedNullDeReference) in method m
  //@ requires a.length > 10;  // ERROR: a might be null!
                ^
1 verification failure

In the above example, the first requires clause might not be well-defined because a might be null. However, if we reverse the order of the clauses, as in the following specification, then the method verifies.

// openjml --esc T_order2.java
//@ nullable_by_default // for the purpose of this example
public class T_order2 {

  //@ requires a != null;
  //@ requires a.length > 10;
  public void m(int[] a) {}

}

old clause

The old clause can compute a value (in the pre-state) that is used elsewhere in the specification. It can thus be used to factor out common subexpressions, to compute something in the pre-state that is used in the postconditions, or to simply make the specification more readable. In the following, the value of g is determined in the pre-state of a call to GCD3, and that value is used again in other that method’s preconditions and in its postcondition.

// openjml --esc --timeout=120 T_Old.java
public class T_Old {

  //@ requires x > 0 && y > 0;
  //@ old \bigint g = Math.gcd(x,y); // spec from Math library
  //@ requires g+g+g <= Integer.MAX_VALUE;
  //@ ensures \result == g+g+g;
  public int GCD3(int x, int y) {
     // some code
     int gcd = mygcd(x,y);
     return gcd+gcd+gcd;
  }

  //@ requires x > 0 && y > 0;
  //@ ensures \result == Math.gcd(x,y); // spec from Math library
  //@ pure
  public int mygcd(int x, int y) {
      return 1; // placeholder
  }
}

Exercises

Follow the link in the above heading to work on the exercises on this topic.

Resources