Monday, November 14, 2011

Runtime Checking of Contracts

As I said before, the most important use of contracts is methodological; by paying attention to contracts, you will be able to avoid many errors you won't have to fix later.  Still, if you go to the trouble of writing contracts, you would like to get additional benefits.  One of the most obvious is runtime checking of contracts, which gives warning about contract violations as they occur, helping catch errors close to their sources.  Without contracts, a bug can corrupt a data structure or its contents, planting a time bomb that can explode much later.  At that point, it is difficult to discover who made the erroneous change even with a debugger, since the offending method is no longer on the stack and can't be examined, and many other traces of the buggy action may also have disappeared.

In order to get these kinds of warnings, the contract must be written in some formal language; typically it is some extension of boolean-valued expressions in the programming language.  Extensions are necessary in order to refer to "old" values; that is, allowing the postcondition to refer to values of variables or expressions on entry to the method.  Rich assertion languages also add ways of expressing universal and existential quantifiers; often, you want to express some property of all the contents of some array or other data structure, or to assert that there is some element with a given property.  However, it is easy to add such capabilities to languages that don't offer them simply by writing appropriate methods to check any required condition.

Runtime contract checking is complicated by several factors.  First is the relationship between contracts on methods in inheritance hierarchies.  As I explained in The Correct Use of Inheritance, inheriting methods may only weaken preconditions and strengthen postconditions.  There are two approaches to enforcing this constraint.  The one used by Eiffel uses syntactic enforcement, in which you can never write assertions violating this rule.  In Eiffel, overriding methods use "ensure then" instead of "ensure" for postconditions, with the meaning that any assertion following "ensure then" is conjoined with any assertions from superclasses.  For example, suppose you have a postcondition "ensure contains(x)" on the method Container.put(x); this ensures that after adding x to the container, it is indeed in it.  A list is a kind of container, and there you want to add the postcondition "ensure then count = old count + 1", which means that the number of elements in the list has increased by one after adding an element.  (This is not the case for sets, which are also containers.)  The full postcondition of List.put(x) is now "contains(x) and then count = old count + 1".  (The "and then" operator is a short-circuit operator, like && in the C family.)  Similarly, preconditions in overriding methods use "require else" rather than "require", and add the new assertions by disjunction ("or else" in Eiffel, || in the C family.)  While this approach prevents any violations of the inheritance rules, it means that you don't see the full contract in the class itself, and there could be hidden assertions you aren't aware of.  This calls for tools that can display the full contract (see Viewing Contracts).

The other approach is to require developers to maintain the correct relationships themselves, by copying assertions as necessary.  In this case, you see the full contract in each class, but need to verify for yourself that the inheritance rules hold in each case.

A runtime assertion-checking tool needs to be aware of the inherited contracts in either approach.  In the first one, it must be aware of the full contract in order to check it properly.  This is less of an issue for postconditions, because these can be checked independently.  But it is crucial for preconditions, since the fact that a precondition written with a certain overriding method is false is not an error if the precondition of the method in some superclass is satisfied.  In the second approach, assertions can be checked for each class independently, but you also want to add checks that warn in case the inheritance rules are violated.

Another complicating factor is the need to keep "old" values, as in the example shown above: "count = old count + 1".  An assertion-checking tool needs to keep the value of count on entry to the method in order to make sure that the value on exit is exactly one more.  The computation of the old value could cause an exception; for example, the Stack.put(x) method may have a postcondition "count > 1 implies item(2) = old item(1)", which means that if after insertion the stack has at least two elements, then the element that used to be on top of the stack ("old item(1)") is now second ("item(2)").  As the tool evaluates the expression item(1) on entry to the method, an exception will occur if the stack is empty.  This, however, is not an error in the program or in the assertions!  What the tool must do is keep a record of the exception, and only raise it if the old value is ever referenced.  This will never happen in this example, because if the stack was initially empty, it will have exactly one element following the put operation, the antecedent "count > 1" of the postcondition will be false, and the consequent that calls for the old value, "item(2) = old item(1)", will never be evaluated.

Yet another challenge is preventing infinite recursion in assertion checking.  For example, if the Stack class has an invariant capacity() >= 0, and this invariant is checked upon entry to the capacity method, an infinite recursion will result.  Eiffel takes a conservative view, and turns off all assertion checking while it checks any assertion.  The rationale for this is that methods used in assertions should be verified separately, before being used to specify the behavior of other parts of the program.  It is possible to check more assertions without getting into an infinite recursion, and various tools have different strategies for dealing with this issue.

Our own assertion-checking tool for Java is called Jose, and uses aspect-oriented programming to handle the issues mentioned above.  More on Jose in a later post!