Contract Programming

Contracts are a breakthrough technique to reduce the programming effort for large projects. Contracts are the concept of preconditions, postconditions, errors, and invariants. Contracts can be done in C++ without modification to the language, but the result is clumsy and inconsistent.

Building contract support into the language makes for:

1. a consistent look and feel for the contracts
2. tool support
3. it's possible the compiler can generate better code using information gathered from the contracts
4. easier management and enforcement of contracts
5. handling of contract inheritance

The idea of a contract is simple - it's just an expression that must evaluate to true. If it does not, the contract is broken, and by definition, the program has a bug in it. Contracts form part of the specification for a program, moving it from the documentation to the code itself. And as every programmer knows, documentation tends to be incomplete, out of date, wrong, or non-existent. Moving the contracts into the code makes them verifiable against the program.

Assert Contract

The most basic contract is the AssertExpression. An assert inserts a checkable expression into the code, and that expression must evaluate to true:

assert(expression);

C programmers will find it familiar. Unlike C, however, an assert in function bodies works by throwing an AssertError, which can be caught and handled. Catching the contract violation is useful when the code must deal with errant uses by other code, when it must be failure proof, and as a useful tool for debugging.

Pre and Post Contracts

The pre contracts specify the preconditions before a statement is executed. The most typical use of this would be in validating the parameters to a function. The post contracts validate the result of the statement. The most typical use of this would be in validating the return value of a function and of any side effects it has. The syntax is:

in
{
  ...contract preconditions...
}
out (result)
{
  ...contract postconditions...
}
body
{
  ...code...
}

By definition, if a pre contract fails, then the body received bad parameters. An AssertError is thrown. If a post contract fails, then there is a bug in the body. An AssertError is thrown.

Either the in or the out clause can be omitted. If the out clause is for a function body, the variable result is declared and assigned the return value of the function. For example, let's implement a square root function:

long square_root(long x)
  in
  {
    assert(x >= 0);
  }
  out (result)
  {
    assert((result * result) <= x && (result+1) * (result+1) >= x);
  }
  body
  {
    return cast(long)std.math.sqrt(cast(real)x);
  }

The assert's in the in and out bodies are called contracts. Any other D statement or expression is allowed in the bodies, but it is important to ensure that the code has no side effects, and that the release version of the code will not depend on any effects of the code. For a release build of the code, the in and out code is not inserted.

If the function returns a void, there is no result, and so there can be no result declaration in the out clause. In that case, use:

void func()
  out
  {
    ...contracts...
  }
  body
  {
    ...
  }

In an out statement, result is initialized and set to the return value of the function.

In, Out and Inheritance

If a function in a derived class overrides a function in its super class, then only one of the in contracts of the function and its base functions must be satisfied. Overriding functions then becomes a process of loosening the in contracts.

A function without an in contract means that any values of the function parameters are allowed. This implies that if any function in an inheritance hierarchy has no in contract, then in contracts on functions overriding it have no useful effect.

Conversely, all of the out contracts needs to be satisfied, so overriding functions becomes a processes of tightening the out contracts.

Invariants

Invariants are used to specify characteristics of a class or struct that always must be true (except while executing a member function). For example, a class representing a date might have an invariant that the day must be 1..31 and the hour must be 0..23:

class Date
{
  int day;
  int hour;

  invariant() {
    assert(1 <= day && day <= 31);
    assert(0 <= hour && hour < 24);
  }
}

The invariant is a contract saying that the asserts must hold true. The invariant is checked when a class or struct constructor completes, at the start of the class or struct destructor. For public or exported functions, the order of execution is:

1. preconditions
2. invariant
3. body
4. invariant
5. postconditions

The code in the invariant may not call any public non-static members of the class or struct, either directly or indirectly. Doing so will result in a stack overflow, as the invariant will wind up being called in an infinitely recursive manner.

Invariants are implicitly const.

Since the invariant is called at the start of public or exported members, such members should not be called from constructors.

class Foo {
  public void f() { }
  private void g() { }

  invariant() {
    f();  // error, cannot call public member function from invariant
    g();  // ok, g() is not public
  }
}

The invariant can be checked with an assert() expression:

1. classes need to pass a class object
2. structs need to pass the address of an instance

auto mydate = new Date(); //class
auto s = S();             //struct
...
assert(mydate);           // check that class Date invariant holds
assert(&s);               // check that struct S invariant holds

Invariants contain assert expressions, and so when they fail, they throw a AssertErrors. Class invariants are inherited, that is, any class invariant is implicitly anded with the invariants of its base classes.

There can be only one Invariant per class or struct.

When compiling for release, the invariant code is not generated, and the compiled program runs at maximum speed.

References

• Contracts Reading List
• Adding Contracts to Java