The previous lesson on model fields described how to use model fields to specify an abstraction. Sometimes model methods can be used instead, though when model fields are applicable they generally are easier to use in specifications and easier to prove facts about in verification. This lesson alters the Polygon example of the previous lesson (which used model fields) to use model methods instead.

At the outset, note that methods used in specifications must be spec_pure (see the section on calling methods in specifications for details), but can be either Java methods or JML methods. One uses a JML method if there is no Java method that accomplishes what is needed. A JML model method is declared just like a Java method except that

  • it is written in a JML annotation
  • it includes the model modifier
  • it need not have an implementation (and generally does not, unless compilation for runtime-assertion-checking is desired).

For example, if the PolygonMM class in the example below did not declare numSides() as a Java method, one could instead add to that class the following declaration, along with its specifications:

//@ model public int numSides();

using model methods

The following is the Polygon example from the tutorial on model fields, altered to use methods — in this case the Java methods are already part of the Polygon interface. However, note that:

  • The datagroup is still needed. When using model methods, one typically will declare standalone datagroups to use in their frame conditions.
  • Reads clauses are needed. They are discussed after the code listing below.
  • If the methods are used within invariants, they typically need to be declared helper and they must not throw exceptions (thus they should be specified using only a public normal_behavior).
  • An abstract method used in modeling typically has no postcondition, or at least not one that fully dictates its value. It is used in proofs as an uninterpreted function, whose value is given by invariants and concrete implementations and the pre- and postconditions in which it is used.
// openjml --esc PolygonMM.java
public interface PolygonMM {
  //@ public normal_behavior
  //@   reads \nothing;
  //@   ensures \result >= 3;
  //@ spec_pure helper
  public int numSides();

  //@ model instance \datagroup allSides;

  //@ public normal_behavior
  //@   reads allSides;
  //@ spec_pure helper
  public int longestSide();

  //@ public invariant numSides() >= 3;

  //@ old int ls = longestSide();
  //@ assignable allSides;
  //@ ensures longestSide() == ls/2;
  public void half();

}

class Square implements PolygonMM {
  //@ also public normal_behavior
  //@  reads \nothing;
  //@  ensures \result == 4;
  //@ spec_pure helper
  public int numSides() { return 4; }

  private int _side; //@ in allSides;

    /*@  public normal_behavior
      @   reads allSides;
      @ also
      @  private normal_behavior
      @   reads _side;
      @   ensures _side == \result;
      @*/
  //@ spec_pure helper
  public int side() {
      return _side;
  }

  //@ public invariant 0 <= side();

  //@ requires 0 <= s;
  //@ ensures side() == s;
  public Square(int s) { _side = s; }

  // specification inherited
  public void half() { _side = _side/2; }

  //@ also public normal_behavior
  //@  requires 0 <= side();
  //@  ensures \result == side();
  //@ spec_pure helper
  public int longestSide() { return _side; }
}

class Triangle implements PolygonMM {
    private int _side1; //@ in allSides;
    private int _side2; //@ in allSides;
    private int _side3; //@ in allSides;

  //@  public normal_behavior
  //@   reads allSides;
  //@ also
  //@  private normal_behavior
  //@   reads _side1;
  //@   ensures \result == _side1;
  //@ spec_pure helper
  public int side1() { return _side1; }

  //@  public normal_behavior
  //@   reads allSides;
  //@ also
  //@  private normal_behavior
  //@   reads _side2;
  //@   ensures \result == _side2;
  //@ spec_pure helper
  public int side2() { return _side2; }

  //@  public normal_behavior
  //@   reads allSides;
  //@ also
  //@  private normal_behavior
  //@   reads _side3;
  //@   ensures \result == _side3;
  //@ spec_pure helper
  public int side3() { return _side3; }

  //@ public invariant side1() <= longestSide() & side2() <= longestSide() & side3() <= longestSide();
  //@ public invariant side1() == longestSide() | side2() == longestSide() | side3() == longestSide();

  //@ ensures side1() == s1 & side2() == s2 & side3() == s3;
  public Triangle(int s1, int s2, int s3) {
    _side1 = s1; _side2 = s2; _side3 = s3;
  }

  //@ also public normal_behavior
  //@  ensures side1() <= \result && side2() <= \result && side3() <= \result;
  //@  ensures side1() == \result || side2() == \result || side3() == \result;
  //@ spec_pure helper
  public int longestSide() { return Math.max(_side1, Math.max(_side2, _side3)); }

  //@ also public normal_behavior
  //@   reads \nothing;
  //@   ensures \result == 3;
  //@ spec_pure helper
  public int numSides() { return 3; }
  
  public void half() { _side1 /= 2; _side2 /= 2; _side3 /= 2; }
}
  
class Test {

  public void test(PolygonMM polygon) {
    int ns = polygon.numSides();
    int p = polygon.longestSide();
    polygon.half();
    int ss = polygon.numSides();
    int pp = polygon.longestSide();
    //@ assert ns == ss;
    //@ assert pp == p/2;
  }

  public void test2(PolygonMM polygon) {
    //@ assert polygon.numSides() == 4; // NOPE - could be any kind of polygon
  }

  public void test3(Square square) {
    //@ assert square.numSides() == 4; // OK
  }

  public void test4(PolygonMM polygon) {
    if (polygon instanceof Square square) {
      //@ assert square.numSides() == 4; // OK as well
    }
  }
}

When the PolygonMM class is checked using OpenJML’s ESC, it produces the following output:

PolygonMM.java:88: verify: The prover cannot establish an assertion (Assert) in method test2
    //@ assert polygon.sides() == 4; // NOPE - could be any kind of polygon
        ^
1 verification failure

reads clauses

When specifying a method like half() that modifies the program state, it is the frame condition (the assignable clause) that tells what part of the program state is modified. Any particular (model) field or array element can be checked to see if it is part of the changed state. If not, the verification system knows that that field was not changed by the method call.

The example code above uses model methods instead of model fields. So in the test() routine, how is it known that polygon.numSides() does not change value upon the call of twice() and that polygon.longestSide() does change? The answer is the reads clause; this clause states what fields a method reads or depends on. The content of the reads clause is a datagroup (and thus may be a model field).

Note that half() assigns to allSides and longestSide() reads allSides. So the value of longestSide() might well be changed by the call of twice() (though not necessarily). We have to look at the postconditions of on longestSide to see what the new value might be. Note that these methods are called on a PolygonMM instance, so nothing is known in test() about the behavior of derived classes.

On the other hand, numSides(), in this example, does not depend on any part of the heap, according to the reads \nothing clause, so its output value will not be changed by half(). Alternately, one might have numSides() read a datagroup nosides. As long as nosides and allSides are disjoint, changes to allSides will still not change the result of numSides().

helper methods

A helper method is one that does not assume that the object’s invariants hold (cf. the lesson on invariants), nor does it ensure that they hold after returning. Methods used in invariant clauses need to be helper methods because otherwise there would be unending recursive calls to check if the invariants are all true. The disadvantage of being a helper method is that sometimes additional pre- or postconditions are needed to assume or assert properties that are otherwise part of the object’s invariants.

Exercises

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

Resources