Programming by Contract Support

The jpf-aprop project supports four annotations that can be used to express program contracts.

• gov.nasa.jpf.annotation.Requires - method preconditions
• gov.nasa.jpf.annotation.Ensures - method postconditions
• gov.nasa.jpf.annotation.Invariant - instance specific class invariants
• gov.nasa.jpf.annotation.StaticInvariant - static class invariants

Each of these annotations can take a variable number of string arguments, which are the expressions to check, e.g.

@Invariant({"d within 40 +- 5",
            "a > 0"})
class SomeType {
  double d = 0; 
  int a = 0;

  @Requires("c > 0")
  @Ensures("Result >= 0")
  public int computeSomething(int c){
    return c - 3;
  }
  ...

To verify the SUT, run JPF either with the gov.nasa.jpf.aprop.listener.ContractVerifier listener

# *.jpf application property file
target= ...
...
listener+=,.aprop.listener.ContractVerifier

or set the appropriate autolisteners. Violations will be reported as normal JPF property violations:

...
====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.AssertionError: invariant violated: "((d within 40+-5) && (a > 0))", values={d=47.0}
        at SomeType.computeSomething(SomeType.java:36)
        ...

Basics

The term "programming by contract" refers to Bertrand Meyers work on  Design by Contract™ (note that this is a trademarked term), which in turn is based on  Hoare triples. The basic idea is simple - treat program executions as contracts between callers and callees: if the caller guarantees certain preconditions, the caller - upon return - will ensure its postconditions.

In other words: preconditions are the caller's responsibility, postconditions are the callee's responsibility.

From a syntactic view, invariants are merely convenience notation for pre- and postconditions that should hold for all public methods of a class. However, pre- and postconditions usually reason about argument and return values, whereas invariants are about field values.

Why not using simple Java assert expressions to do this, like

...
public int computeSomething (int c){
  assert c>0 : "argument value precondition violated";
  ..res = ...
  assert res>=0 : "return value postcondition violated";
  return res;
}
...

Apart from that it would be rather tedious to have such assertions in every method (e.g. for invariants), it would be easy to forget them in some places (e.g. postconditions for method with several exit points) and might require finally blocks on all postconditioned methods.

Another shortcoming is that assertion expressions would be evaluated within the SUT, i.e. can change its behavior. To avoid a lot of duplication for invariants, these are usually factorized into dedicated methods, which might easily hide the requirement that they should not have side effects.

The explicit assertion approach really falls apart if it comes to class inheritance and polymorphism. The question at hand is what to do in the presence of pre- and postconditions for overridden methods. Assume we have two classes

class A {
  @Requires("arg >= 0")              // (1)
  @Ensures("Result > 0")             // (2)
  int foo (int arg){..}
  ...
}
...
class B extends A {
  @Requires("arg > 1")               // (3)
  @Ensure("Result > 2")              // (4)
  int foo (int arg){..}
  ...
}

Assume further the SUT contains code like

    B b = new B();
    ...
    int x = 42 / (b.foo(2) -2);      // (5)  satisfies (3) => (4)
  ...
    A a = b;
    ...  
    int x = 42 / a.foo(0);           // (6)  satisfies (1) => (2)

Both foo() call sites are conforming to the contracts they see. (5) only knows about the contracts from class B, it fulfills (3) and hence takes (4) for granted. (6) only knows about class A, not the concrete type of the object, and hence assumes everything is fine if it fulfills (1). It would be very confusing if (6) would result in an exception because of the unknown concrete type B of the object referenced by a.

The callee B.foo() on the other hand doesn't know about its caller and hence - if its preconditions are met - has to guarantee all postconditions a potential callers might see, which means its own and all the overridden postconditions of its super classes.

The conclusion is the "weakening precondition, strengthening postcondition" principle. A precondition is fulfilled if either the precondition of the overriding method or any of the preconditions of the methods it overrides is true. A postcondition is fulfilled if all postconditions of overriding and overridden methods are true.

This means we have to look at both sub- and super-contracts to determine if a contract is fulfilled. With normal assertion expressions, this would either force us to accumulate all super-contracts in an overriding method (tedious, fragile), or to refactor all pre- and postconditions into methods of their own, effectively doubling the number of methods in a class. Both approaches are not practical.

As a consequence, there are mostly two ways inheritance-aware contracts can be implemented without bloating the SUT with lots of dedicated contract methods

• as a compiler that emits SUT code for contract expressions
• in a dedicated runtime system that evaluates contract expressions outside the SUT

The second approach is the one we take with JPF, which also ensures absence of side effects of contract expression evaluation with respect to SUT behavior. This meets one of the most prominent flight software verification principles of NASA: "test what you fly, fly what you test".

Last not least it should be mentioned that contracts - as part of the interface specification of a class - are also useful program documentation. Developers using code that has preconditions can see what assumptions the called code has about its calling environment. Developers creating derived classes can see what postconditions overridden methods guarantee, to make sure their implementations stay consistent. Without explicit pre-, postconditions and invariants such information has to be extracted from the code and therefore often gets lost.

Contract Expression Language

Implementing contracts as annotations requires contract expressions to be specified as literal arguments, such as

  @Requires({"a > 40", "b < 50"})

While this has the drawback of expressions not being checked at compile time, it also comes with the silver lining that we can introduce our own grammar for contracts. Why would that be a good idea? As mentioned above, contracts are also meant to be program documentation. Their syntax therefore should be as simple, readable and conscious as possible. Instead of a specification like

  assert d >= 40.0 && d <= 50.0 

we can use our own expressions with runtime type inference

  @Requires(" d within 45 +- 5")

We can especially add generic expression that allows us to introduce new properties such as

  @Ensures("Result satisfies IsMonotonicDecreasing")
  int computeSomething(..){..}

where IsMonotonicDecreasing is a class that is provided at JPF runtime. Since annotation arguments (String literals) do not cause SUT compilation to fail, contract property implementation can be postponed and extended.

The current contract language is implemented with the  Antlr parser generator, a complete grammar is attached to this page. Contract expressions are mostly value comparisons that currently support

• method argument names (for pre- and postconditions)
• field names of the annotated class (and its super classes)
• numeric constants (42, 42.0, 0.42e1)
• quote '..' delimited string literals ('this is a string', note that you can't use double quotes because this is within a string literal Java annotation argument)
• Result as a generic name for a method return value
• old (var) as a generic name for the value of a method argument or field value upon method entry (postconditions)
• logical operators for contract expressions a || b, a && b
• nested contract expressions in parenthesis a && (b || c)
• EPS for some configured precision of a floating point computation
• the usual comparators ==, !=, >, >=, '<', <=
• interval comparators "within x +- d" or "within x,y"
• collection tests isEmpty and notEmpty
• type checks "instanceof type"
• regular expression matchers for string values "matches regex"
• a generic "satisfies propertyClass" operator
• numeric expressions for argument and field variables using +, -, *, /
• some numeric functions like log(x), log10(x)

Examples of valid contract specifications are

@Invariant({"d within 40 +- 5",
            "a > 0"})
public class A {
  double d = 0;
  int a = 0;
  ...

  @Requires("c > 0")
  @Ensures("Result >= 0")
  public int foo(int c){..}

  @Ensures("Result satisfies IsMonotonicDecreasing")
  int computeSomething(..) {..}

  @Requires("a within -10,10")
  @Ensures("old(d) >= d")
  int baz(int a) {..}

  @Ensures("Result matches '[0-9].*X'")
  String getCode(..){..}
  ...

Contract predicates can be both defined inside the SUT and at the listener level.

class MySutClass {
  @Ensures("Result satisfies IsMonotonicDecreasing")  // SUT external predicate
  int computeSomething(..) {..}

  @Ensures("Result satisfies ContractTest$IsValidDate('01/01/1999', '12/31/2010')")
  Date computeDate(..) {..}

  @SandBox // means it's not allowed to change anything but its own fields (side effect free)
  static class IsValidDate implements Predicate {
    public String evaluate (Object testObj, Object[] args) {
      ... // return null if Ok, error message otherwise
    }
  }
  ...

Note that property classes within the SUT have to be carefully checked for side effects. The SandBox property comes in handy for this. Implementing native predicate classes looks like this

public class IsMonotonicDecreasing implements NativePredicate {
  Number lastNumber; // NOTE - reset when backtracking
  ...
  public String evaluate(Object testObj, Object[] args) {
    if (!(testObj instanceof Number)) {
      throw new ContractException("IsMonotonicDecreasing test object not a Number: " + testObj);
    }

    Number num = (Number)testObj;
    ...

      if (lastNumber.doubleValue() < num.doubleValue()) {
        return ("IsMonotonicDecreasing failed: " + lastNumber + ", " + num);
    }
    ...
    lastNumber = num;
    return null; // satisfied
  }

Predicate instances usually have their own state (e.g. lastNumber), which might have to be restored upon backtracking. Native predicate classes have to be in the native_classpath, i.e. require JPF configuration.

The contract expression language is supposed to evolve, but it will remain centered around properties that can be checked upon method invocation and return. Safety properties that relate to the method execution itself will be implemented with dedicated listener/annotation pair, such as

@MaxInstructions(1000) 
void foo(..){..}

@NoAllocation
void bar(..){..}

@NonBlocking
void baz(..){..} 

This is possible because the contract verification is implemented as a JPF listener that can coexist with other property listeners.

Exceptional postconditions are not implemented yet.

Implementation

Contract management and evaluation is implemented in the listener class gov.nasa.jpf.aprop.ContractVerifier. This JPF listener mostly reacts on

• executeInstruction notifications, to check postconditions and invariants for ReturnInstructions
• instructionExecuted notifications, to check preconditions and to store old(..) values for InvokeInstructions

Invariants get parsed by the  Antlr generated ContractSpecParser upon classLoaded notifications. Method pre- and postconditions get parsed on demand when encountering InvokeInstructions. Parsed contract expressions get stored as Contract objects in HashMaps under the corresponding MethodInfo or ClassInfo keys, to make sure they only have to be parsed once.

Contract instances are basically ASTs, their evaluation follows the  Interpreter pattern. All AST node classes reside in package gov.nasa.jpf.aprop.