digitalmars.com                        
Last update Fri Apr 4 16:44:16 2014

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. Digital Mars introduces the first C and C++ compiler to support contracts.

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.

Contracts in Digital Mars C/C++ introduce the following new keywords:

__in
__out
__body
__invariant (for C++)

If contracts become adopted by the ANSI standards, the keywords will likely lose the __ prefix, so it is best to assume that in, out, body and invariant will become keywords.

Contracts are enabled by throwing the -D compiler switch. If the -D switch is not thrown, the contract code is not generated or executed. Source files with contracts compiled with -D can be freely intermingled with source files with contracts not compiled with -D.

Assert Contract

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

assert(expression);

C/C++ programmers will find this familiar - it's already in the language. The Digital Mars contract extensions use the assert as the fundamental building block of contracts.

Pre and Post Contracts

The pre contracts specify the preconditions before a function body 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 function, which are its return value and any side effects. The syntax is:

function declaration(parameters)
__in
{
    ...contract preconditions...
}
__out (result)
{
    ...contract postconditions...
}
__body
{
    ...code...
}

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

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);
  }
  __body
  {
    return sqrt(x);
  }

The assert's in the in and out bodies are the specific contracts. Any other C/C++ statement or expression is allowed in the bodies, but it is important to make sure that such code has no side effects, so 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
  {
    ...
  }

Class Invariants (C++ only)

Class invariants are used to specify characteristics of a class 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:

struct Date {
  int day;
  int hour;

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

The class invariant is a contract saying that the asserts must hold true. The invariant is checked when a class constructor completes, at the start of the class destructor, before a public member is run, and after a public function finishes. Class invariants are inherited, that is, any class invariant is implicitly anded with the invariants of its base classes. Class invariant functions can be declared virtual, and as a general rule, they should be virtual if and only if the class destructor is virtual.

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

Future Directions with DBC

These are some issues that will be addressed in the future with the DBC feature in DMC++. Anticipate these changes when writing contract code.

If the function is virtual, the __in clause needs to be OR'd with the __in clauses of any functions it overrides in all the base classes. Similarly, the __out clause needs to be AND'd with all the __out clauses.

__in clauses should not be able to modify the function parameters.

When an __out clause references a function parameter, the value should be the same as when the function was called, and not what it is after the function body may have modified it.

Currently, contracts rely on the assert() macro aborting the program with a message. Perhaps this needs to be revisited, and changed to throw an exception instead.

Legacy Compilers

Contract code can be ported to legacy compilers by using #ifdef's:

void foo()
#ifdef __DMC__
  __in
  {
    ...
  }
  __body
#endif
  {
  }

References

Home | Runtime Library | IDDE Reference | STL | Search | Download | Forums