# 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 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
}
}
}
```

`Polygon`

is 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
}
}
}
```