When writing specifications for an abstract parent class or interface and a concrete derived class, the parent class needs to express its properties in terms of some abstract quantities. Model fields can be used to describe the properties of an abstract class and datagroups are used as an abstraction of frame conditions.

Using model fields

Model fields:

  • Model fields are specification-only fields that encapsulate some property of a class (typically, but not necessarily, an abstract class or interface).
  • The model field can be used in the specification of the abstract class.
  • A model field is given an implementation by writing a represents clause in the derived class; this connects the model field to the concrete implementation.
  • A model field can also be used within a concrete class to represent some characteristic that is not explicitly present in the concrete class.
  • A model field is typically an instance field. Java only allows static fields in an interface. But in JML one can declare instance model fields in an interface (or class) using the modifier instance. As the (Java) default is static for field declarations, the instance keyword is required in this case.

Datagroups:

  • A model field is also a datagroup; or a standalone datagroup (not associated with an abstract value) can be declared using the type JMLDataGroup.
  • A datagroup is an abstraction of a frame condition.
    • In the abstract class the datagroup can be used in a frame condition
    • In the concrete class specific fields can be declared to be in that datagroup

Here is a working example that verifies, with commentary below.

// openjml --esc Polygon.java
interface Polygon {
  //@ model instance public int sides;
  //@ model instance public int longestSide;

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

  //@ requires longestSide < 10000;
  //@ assigns longestSide;
  //@ 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 Polygon {
  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 Test {
  //@ requires polygon.longestSide < 10000;
  public void test(Polygon 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(Polygon 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(Polygon polygon) {
    if (polygon instanceof Square square) {
      //# assert square.sides() == 4; // OK as well
    }
  }
}
  • Polygonis an (abstract) interface with a concrete implementation Square
  • Polygon declares two properties, as model fields: sides (the number of sides) and longestSide (the length of the longest side of the polygon)
  • There is an invariant limiting the length of the sides and another one saying that all polygons have at least 3 sides.
  • There are two simple methods that return the values of sides and longestSide. These are pure (do not change anything).
  • The method twice doubles the size of the polygon.
    • It has a precondition so that the resulting polygon still satisfies the invariant.
    • It has an assigns clause saying what is modified.
    • It has a postcondition saying what happens to the memory locations that are modified.

Square is an implementation of Polygon:

  • Square has just one data member, side (the length of a side of the square)
  • The constructor for Square initializes side; it needs a precondition in order to satisfy the invariant for Polygon, which applies to Square by inheritance.
  • The clause represents sides = 4 gives a value to the sides model field in Polygon
  • The clause represents longestSide = side gives a value to the longestSide model field using concrete fields of Square
  • And the side field is declared to be in longestSide. When twice (abstractly) assigns to the model field longestField, then all the fields that are in longestField are considered assigned to.
  • Then all the methods that Square inherits from Polygon are implemented as expected, but they can inherit all their specifications from Polygon. No additional specifications are needed. Look at sides() as an example: the specification says it returns the value of sides, which is given a value by the represents clause, so the implementation of Square.sides() satisfies the abstract specification given for Polygon.sides().

Test just checks that the specifications given for Polygon work to verify some simple uses of the interface and its specifications.

  • Note that the implementation and verification of Test.test() only use Polygon and its specifications.
  • The assert in test2 fails because a polygon (as implemented) can have a variety of numbers of sides.
  • But the assert in test3 succeeds, because a Square knows how many sides it has.
  • In test4() we do a type test to see if the input polygon is a Square, and if so, we know how many sides it has.

The output when verifying the example above (though you may want to add the --progress option) is this:

Polygon.java:52: 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

Using datagroups

In the above example, longestSide does not quite properly capture the effect of twice(), which alters the lengths of all of the sides, not just the longest one. The following code separates the datagroup aspect of longestSide into a more general, standalone, datagroup named allSides. This code is only slightly different than the previous listing. In particular, Square and Test are precisely the same. But now an implementation of another derived class, Triangle (with three different sides) is clearer: put all three sides in allSides and make the implementation of longestSide be the maximum of the three sides.

// 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
    }
  }
}