JML Tutorial - Inheriting Specifications
In classic object-oriented design, a base class, perhaps abstract, can be used without knowing what kind of derived class it dynamically is. One can talk about a Shape’s perimeter or area without needing to know what kind of Shape it is. When we write specifications for the base class we define its behavior and then any derived class is expected to adhere to that behavior. This property is called behavioral inheritance. JML enforces it by insisting that derived classes inherit the behavior of base classes, by inheriting their specifications.
Here is a simple example:
// openjml --esc T_Polygon.java
public interface T_Polygon {
//@ ensures \result > 0;
//@ pure helper
public int sides();
}
class Square implements T_Polygon {
//@ public invariant side >= 0;
public int side;
//@ requires 0 <= side < 1000;
//@ ensures this.side == side;
public Square(int side) {
this.side = side;
}
//@ also ensures \result == 4;
//@ pure helper
public int sides() {
return 4;
}
}
In this example T_Polygon
is an interface with a method that returns a property of a polygon. Even though the method is abstract, we can state some
properties: a polygon has some positive number of sides. Then Square
is a concrete class that implements
T_Polygon
. Now those abstract methods have an implementation.
- The method in
Square
inherits the specification from its counterpart inT_Polygon
- The keyword
also
at the beginning of the specification ofsides()
inSquare
is a visual indicator that there are additional specifications in parent classes or interfaces (much like the annotation@Override
does in Java). - The method
sides()
inSquare
ends up with two behaviors (in the sense of the discussion in the lesson on multiple behaviors). - The method
sides()
inSquare
must satisfy each of its behaviors independently - Any methods in
T_Polygon
have no implementation (because they are abstract methods of an interface), so there is nothing to verify about them. However their interfaces will be checked when verifying any derived class.
When the methods of T_Polygon
are called in some client class, the client class knows the properties based on the (static) type of the reference it has.
For example,
// openjml --esc T_PolyTest.java T_Polygon.java
public class T_PolyTest {
public void test(T_Polygon poly) {
int i = poly.sides();
//@ assert i > 0; // OK -- property of all T_Polygon instances
//@ assert i == 4; // NO -- who knows what kind of polygon it is
}
public void test2(Square sq) {
int i = sq.sides();
//@ assert i > 0; // OK - true of all T_Polygon instances
//@ assert i == 4; // OK - true of Square instances
}
}
produces
T_PolyTest.java:7: verify: The prover cannot establish an assertion (Assert) in method test
//@ assert i == 4; // NO -- who knows what kind of polygon it is
^
1 verification failure
In test()
, only the properties of a T_Polygon
are known; after all, any kind of T_Polygon
instance might have been passed in.
But in test2()
, we know it is a Square
, so the assertions pass now.
We can also check the type of the input T_Polygon
. If we know it is a Square
then we can prove the more specific properties.
This version verifies fine:
// openjml --esc T_PolyTest2.java T_Polygon.java
public class T_PolyTest2 {
public void test(T_Polygon poly) {
if (poly instanceof Square sq) {
int i = sq.sides();
//@ assert i > 0; // OK -- property of all T_Polygon instances
//@ assert i == 4; // OK -- this T_Polygon is a Square
}
}
}
This simple example is intended only to show specification inheritance. The next two lessons on specification with model fields and model methods, show more complex examples that specify abstract classes.