Last Modified:

Pure methods

The specifications we have written so far have contained just simple expressions and operators. It is also convenient, and allowed, to call methods in specifications — but there are restrictions.

Expressions in specifications must not have any effect on the Java program. Think of a program with specifications converted to run-time checks. We can’t have the checks modifiying the program that is being checked. Similarly we can’t allow static checking to have any effect on the Java program.

Thus the rule is that methods that are called in specifications must be pure, that is, must not have any side-effects. In fact JML requires that a method used in specifications be marked with the modifier pure. And if a method is pure, it automatically includes the specification clause assigns \nothing;.

Here is an example:

// openjml --esc T_PureMethod1.java
public class T_PureMethod1 {

  public static class Counter {
    //@ spec_public
    private int count;

    //@ spec_public
    final private int maxCount;

    //@ requires max >= 0;
    //@ ensures count == 0 && maxCount == max;
    //@ pure
    public Counter(int max) {
      count = 0;
      maxCount = max;
    }

    //@ requires count < maxCount;
    //@ assigns count;
    //@ ensures count == \old(count+1);
    public void count() { ++count; }

    //@ ensures \result == (count > 0);
    //@ pure
    public boolean isAnythingCounted() {
       return count > 0;
    }

    //@ ensures \result == !(count < maxCount);
    public boolean atMax() {
       return count >= maxCount;
    }
  }

  public void test() {
    Counter c = new Counter(2);
    //@ assert !c.isAnythingCounted() && !c.atMax();
    c.count();
    //@ assert c.isAnythingCounted() && !c.atMax();
    c.count();
    //@ assert c.isAnythingCounted() && c.atMax();
  }
}

Running OpenJML produces

T_PureMethod1.java:38: warning: A non-pure method is being called where it is not permitted: T_PureMethod1.Counter.atMax()
    //@ assert !c.isAnythingCounted() && !c.atMax();
                                                 ^
T_PureMethod1.java:40: warning: A non-pure method is being called where it is not permitted: T_PureMethod1.Counter.atMax()
    //@ assert c.isAnythingCounted() && !c.atMax();
                                                ^
T_PureMethod1.java:42: warning: A non-pure method is being called where it is not permitted: T_PureMethod1.Counter.atMax()
    //@ assert c.isAnythingCounted() && c.atMax();
                                               ^
3 warnings

The call of c.isAnythingCounted is allowed in the specification because it is declared pure in its specification. However c.atMax() is not allowed because it is not declared pure. If you add that modifier to the declaration of atMax then this example will verify (cf. example T_PureMethod2.java).

Notice that these pure methods have no assigns clause. Pure methods are not allowed to write to any fields, so if there were an assigns clause it would have to be assigns \nothing;. In fact, for a pure method, the default assigns clause is precisely that assigns \nothing;. (For a non-pure method, the default is assigns \everything;.)

If you add a pure modifier to count (as in T_PureMethod3.java), then OpenJML produces

T_PureMethod3.java:20: error: Pure methods may not assign to any fields: count in T_PureMethod3.Counter.count()
    //@ assigns count;
                ^
1 error

It is also vitally important to remember that when a method is used in a specification, it is the specification of the method that is used to determine its behavior, not its implementation.

This example

// openjml --esc T_PureMethod4.java 
public class T_PureMethod4 {

  //@ requires i > Integer.MIN_VALUE;
  //@ ensures \result >= 0;
  //@ pure
  public static int abs(int i) {
    return i >= 0 ? i : -i;
  }

  public void test(int k) {
    //@ assert k >= 0 ==> abs(k) >= k;
  }
}

produces this output:

T_PureMethod4.java:12: verify: The prover cannot establish an assertion (Assert) in method test
    //@ assert k >= 0 ==> abs(k) >= k;
        ^
1 verification failure

This abs function verifies successfully; however, the assertion that uses it in test does not. That is because all that the method test knows about the result of abs is that it is greater than zero. In order to verify test, the postcondition of abs must be strengthened to say that if i>0 then the result is the same as the input.

Methods do not always need to have precise functional specs. However, the specification does need to be strong enough to verify whatever uses the clients of the method need.

Well-defined method calls

The lesson on well-defined expressions described how expressions in specifications must be well-defined. For a method call within a specification clause, that means two things: (a) the pre-conditions of the method must be fulfilled and (b) the method may not throw any exceptions.

The next example shows the kind of error message that OpenJML produces when a method’s precondition is not fulfilled:

// openjml --esc T_PureMethod5.java 
public class T_PureMethod5 {
  //@ spec_public
  int[] a = new int[10];

  //@ requires 0 <= i & i < a.length;
  //@ ensures \result == a[i];
  //@ pure
  public int elementAt(int i) {
    return a[i];
  }

  public void test1() {
    //@ assert elementAt(0) == 0;
  }

  public void test2() {
    //@ assert elementAt(-1) == 0;
  }
}

produces

T_PureMethod5.java:14: verify: The prover cannot establish an assertion (Assert) in method test1
    //@ assert elementAt(0) == 0;
        ^
T_PureMethod5.java:14: verify: The prover cannot establish an assertion (UndefinedCalledMethodPrecondition: T_PureMethod5.java:9:) in method test1
    //@ assert elementAt(0) == 0;
                        ^
T_PureMethod5.java:9: verify: Associated declaration: T_PureMethod5.java:14:
  public int elementAt(int i) {
             ^
T_PureMethod5.java:6: verify: Precondition conjunct is false: i < a.length
  //@ requires 0 <= i & i < a.length;
                          ^
T_PureMethod5.java:18: verify: The prover cannot establish an assertion (UndefinedCalledMethodPrecondition: T_PureMethod5.java:9:) in method test2
    //@ assert elementAt(-1) == 0;
                        ^
T_PureMethod5.java:9: verify: Associated declaration: T_PureMethod5.java:18:
  public int elementAt(int i) {
             ^
T_PureMethod5.java:6: verify: Precondition conjunct is false: 0 <= i
  //@ requires 0 <= i & i < a.length;
                 ^
7 verification failures

The relevant error messages include the term ‘Undefined’ to indicate that this instance of an out of range index is part of a specification instead of in Java code. Note that the elementAt method here verifies; it is the use of it that is at fault.

Termination and Exceptions

Methods marked pure so they can be used in specifications must satisfy two additional properties. First they must be terminating. The specification diverges false; states this property for a method, but as it is the default, it does not need to be written. See the advanced lesson on termination for more on this topic.

The other property is that when a method is used in a specification it is assumed not to throw any exceptions. It is best if the method has only normal_behavior specification cases, but if it has any exceptional_behavior cases, they will be ignored for use in specifications. (cf. Multiple Behaviors)

Pure constructors

You might have noticed that the constructor for Counter in the example above is also marked pure. Constructors create new objects or arrays, so they are not allowed to be used in specifications. Nevertheless, it is helpful to mark a constructor as pure to indicate that the constructor does not modify any memory other than setting its own fields.

Pure classes

A class can also be marked pure. This means that all the constructors and methods of the class are themselves pure. This is a useful part of specifying an immutable class, one whose objects may not be changed after being created. Java’s String and Integer are two examples of immutable classes.

Using Method Calls in Specifications Problem Set