The previous lesson 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. This lesson alters the example of the previous lesson to use methods instead.

At the outset, note that methods used in specifications must be pure (cf. here), 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, except if compilation for runtime-assertion-checking is desired).

For example, if the example below did not declare sides() as a Java method, one could include in Polygon3 this declaration, along with any specifications:

//@ model public int sides();

using model methods

Here is the model field example, altered to use methods — in this case the Java methods already part of the Polygon interface. There are a few key points to note:

  • The datagroup is still needed. When using model methods, one typically will declare standalone datagroups to use in frame conditions.
  • Reads clauses are needed. They are discussed after the code listing.
  • If the methods are used within invariants, they typically need to be declared helper and that they do not throw exceptions (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 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 Polygon3.java
interface Polygon3 {
  //@ model instance public int sides;
  //@ model instance public JMLDataGroup allSides;
  //@ model instance public int longestSide; //@ in allSides;

  //@ public invariant 0 <= longestSide < 20000;
  //@ public invariant sides >= 3;

  //@ requires longestSide < 10000;
  //@ assigns allSides;
  //@ ensures longestSide == \old(longestSide) + \old(longestSide);
  public void twice();

  //@ ensures \result == sides; pure
  public int sides();

  //@ ensures \result == longestSide; pure
  public int longestSide();
}
class Square implements Polygon3 {
  public int side; //@ in longestSide;

  //@ public represents sides = 4;
  //@ public represents longestSide = side;

  //@ requires 0 <= s < 20000;
  //@ ensures side == s && sides == 4;
  public Square(int s) { side = s; }

  // specification inherited
  public void twice() { side = side+side; }

  // specification inherited; cf the represents clause for sides
  public int sides() { return 4; }

  // specification inherited; cf the represents clause for longestSide
  public int longestSide() { return side; }
}
class Triangle implements Polygon3 {
  public int side1; //@ in longestSide;
  public int side2; //@ in longestSide;
  public int side3; //@ in longestSide;

  //@ public invariant 0 <= side1 && 0 <= side2 && 0 <= side3;
  //@ public invariant side1 <= longestSide && side2 <= longestSide && side3 <= longestSide;

  //@ requires 0 <= s1 < 20000 && 0 <= s2 < 20000 && 0 <= s3 < 20000;
  //@ ensures this.side1 == s1 && this.side2 == s2 && this.side3 == s3;
  public Triangle(int s1, int s2, int s3) { side1 = s1; side2 = s2; side3 = s3; }

  //@ public represents sides = 3;
  //@ public represents longestSide = Math.max(side1, Math.max(side2, side3));
  
  public int longestSide() { return Math.max(side1, Math.max(side2, side3)); }

  public int sides() { return 3; }

  public void twice() { side1 += side1; side2 += side2; side3 += side3; }
}
  
class Test {
  //@ requires polygon.longestSide < 10000;
  public void test(Polygon3 polygon) {
    int s = polygon.sides();
    int p = polygon.longestSide();
    polygon.twice();
    int ss = polygon.sides();
    int pp = polygon.longestSide();
    //@ assert s == ss;
    //@ assert 2*p == pp;
  }

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

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

  public void test4(Polygon3 polygon) {
    if (polygon instanceof Square square) {
      //# assert square.sides() == 4; // OK as well
    }
  }
}

reads clauses

When specifying a method like twice() that modifies the program state, it is the frame condition (the assigns 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.sides() 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 may be a model field.

Note that twice() assigns to allSides and longestSide() reads allSides. So the value of longestSide() might well be changed by the call of twice() (though not necessarily). But sides() reads the model field numSides, which is not assigned by twice(), so its value does not change.

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.