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 spec_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 PolygonMM 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 are 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 PolygonMM.java
public interface PolygonMM {
  //@ model instance public \datagroup allSides;

  //@ public normal_behavior
  //@   reads \nothing;
  //@   ensures \result >= 3;
  //@ spec_pure helper
  public int sides();

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

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

  //@ old int s = longestSide();
  //@ assigns allSides;
  //@ ensures longestSide() == s/2;
  public void half();

}
class Square implements PolygonMM {
  public int side; //@ in allSides;

  //@ 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
  //@  reads \nothing;
  //@  ensures \result == 4;
  //@ spec_pure helper
  public int sides() { return 4; }

  //@ also public normal_behavior
  //@  requires 0 <= side;
  //@  ensures \result == side;
  //@ spec_pure helper
  public int longestSide() { return side; }
}
class Triangle implements PolygonMM {
  public int side1; //@ in allSides;
  public int side2; //@ in allSides;
  public int side3; //@ in allSides;

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

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

  //@ also public normal_behavior
  //@  ensures \result >= side1 && \result >= side2 && \result >= side3;
  //@  ensures \result == side1 || \result == side2 || \result == side3;
  //@ 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 sides() { return 3; }

  
  public void half() { side1 /= 2; side2 /= 2; side3 /= 2; }
}
  
class Test {

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

  public void test2(PolygonMM 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(PolygonMM polygon) {
    if (polygon instanceof Square square) {
      //@ assert square.sides() == 4; // OK as well
    }
  }
}

which produces this 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 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 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 nothiing is known in test() about the behavior of derived classes.

On the other hand, sides(), 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 sides() read a datagroup numsides. As long as numsides and allSides are disjoint, changes to allSides will still not change the result of sides().

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.