JML Tutorial - Model Fields and Datagroups
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 isstatic
for field declarations, theinstance
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
}
}
}
Polygon
is an (abstract) interface with a concrete implementationSquare
Polygon
declares two properties, as model fields:sides
(the number of sides) andlongestSide
(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
andlongestSide
. 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
initializesside
; it needs a precondition in order to satisfy the invariant forPolygon
, which applies toSquare
by inheritance. - The clause
represents sides = 4
gives a value to thesides
model field inPolygon
- The clause
represents longestSide = side
gives a value to thelongestSide
model field using concrete fields ofSquare
- And the
side
field is declared to be inlongestSide
. Whentwice
(abstractly) assigns to the model fieldlongestField
, then all the fields that are inlongestField
are considered assigned to. - Then all the methods that
Square
inherits fromPolygon
are implemented as expected, but they can inherit all their specifications fromPolygon
. No additional specifications are needed. Look atsides()
as an example: the specification says it returns the value ofsides
, which is given a value by the represents clause, so the implementation ofSquare.sides()
satisfies the abstract specification given forPolygon.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 usePolygon
and its specifications. - The
assert
intest2
fails because a polygon (as implemented) can have a variety of numbers of sides. - But the
assert
intest3
succeeds, because aSquare
knows how many sides it has. - In
test4()
we do a type test to see if the inputpolygon
is aSquare
, 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
}
}
}