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 in T_Polygon
  • The keyword also at the beginning of the specification of sides() in Square 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() in Square ends up with two behaviors (in the sense of the discussion in the lesson on multiple behaviors).
  • The method sides() in Square 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.