A method’s specification states what the method does, but not how it is done. What a method does is stated in its postcondition, which is written in one (or more) ensures clause(s). Such postconditions are asserted as a method is returning.

(Ensures clauses may be mixed in any order with its requires clauses, but good, and clearer, style suggests putting all requires clauses first and then all ensures clauses.)

Consider this example of a method that computes the maximum of four int values.

// openjml --esc T_ensures1.java
public class T_ensures1 {
  //@ ensures \result == a | \result == b | \result == c | \result == d;
  //@ ensures \result >= a & \result >= b & \result >= c & \result >= d;
  public int max4(int a, int b, int c, int d) {
    if (a > b) {
        if (c > d) {
            if (a > c) return a;
            else       return c;
        } else {
            if (a > d) return a;
            else       return d;
        }
    } else {
        if (c > d) {
            if (b > c) return b;
            else       return c;
        } else {
            if (b > d) return b;
            else       return d;
        }
    }
  }
}

The ensures clauses just prior to the method declaration state two properties that are expected to hold about the result, which is designated by the keyword \result.

  • The result must be equal to (at least) one of the four inputs.
  • The result must be greater than or equal to each of the four inputs.

The body of the function computes this result. Note that the specification states the properties of the result but does not state how it is computed. In fact, the same specification could be used with a different implementation:

// openjml --esc T_ensures1a.java
public class T_ensures1a {
  //@ ensures \result == a | \result == b | \result == c | \result == d;
  //@ ensures \result >= a & \result >= b & \result >= c & \result >= d;
  public int max4(int a, int b, int c, int d) {
    if (a >= b && a >= c && a >= d) return a;
    if (b >= a && b >= c && b >= d) return b;
    if (c >= a && c >= b && c >= d) return c;
    return d;
  }
}

Both of the above examples verify as correct with respect to the given specifications.

Now consider a third example:

// openjml --esc T_ensures2.java
public class T_ensures2 {
  //@ ensures \result == a | \result == b | \result == c | \result == d;
  //@ ensures \result >= a & \result >= b & \result >= c & \result >= d;
  public int max4(int a, int b, int c, int d) {
    if (a > b) {
        if (c > d) {
            if (a > c) return a;
            else       return c;
        } else {
            if (a > d) return a;
            else       return d;
        }
    } else {
        if (c > d) {
            if (b > c) return b;
            else       return c;
        } else {
            if (b > c) return b;   // ERROR: see text!
            else       return d;
        }
    }
  }
}

ESC produces the following output for the above code.

T_ensures2.java:19: verify: The prover cannot establish an assertion (Postcondition: T_ensures2.java:4:) in method max4
            if (b > c) return b;   // ERROR: see text!
                       ^
T_ensures2.java:4: verify: Associated declaration: T_ensures2.java:19:
  //@ ensures \result >= a & \result >= b & \result >= c & \result >= d;
      ^
2 verification failures

The error message tells us that the specification and implementation are not consistent; in particular, the ensures clause on line 4 is not satisfied when the method exits on line 19. Some code inspection reveals that there is an error in the if condition on line 19: it should be b > d (as it is in example T_ensures1.java above). This is the kind of cut-and-paste error that can be easy to miss during code inspection.

OpenJML is able to provide more debugging information than just the error message. Tutorial examples are given under the debugging topic.

While in this case the error was in the implementation, the error might instead be in the specification. In fact, it is possible that the specification and implementation agree, but that they both differ from what the user intended.

Another situation can be that the specification is not very specific. For example, the postcondition could simply be ensures true;, which is the default if no ensures clause is given. In this case the implementation trivially satisfies the specification, no matter what the implementation does to make the final state of an execution. However, while no problem arises in verifying the method, it would not be possible to verify uses of the method in some calling method (unless it indeed did not matter what the method does). We will return to this subject in Calling Specified Methods.

Sometimes you may wish to refer to the value returned by a method in the postcondition. This value is referenced as \result. Like all JML keywords in expression, \result begins with a backslash so it will not conflict with a Java identifier. \result may only be used in ensures clauses of method specifications for methods that return values (and not for constructors). Here is a simple example:

// openjml --esc T_ensures3.java
public class T_ensures3 {
  //@ requires a.length > 0;
  //@ ensures \result == a[0];
  public int first(int[] a) {
    return a[0];
  }
}

Two final points:

  • The order of ensures clauses matters. The predicates of a sequence of ensures clauses are effectively conjoined together (with &&) to produce a single postcondition predicate. Consequently an earlier predicate may be needed to make a later predicate be well-defined.
  • In thinking about postconditions, be aware of the semantics of the ensures clause, namely, if the method terminates normally (without an exception or error), then the given postcondition must be true. The converse, if the ensures predicate is true then the method terminates normally, is not the meaning and is not necessarily true.

Exercises

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

Resources