Proposal to add Contract Programming to C++ (revision 1)

Author: Thorsten Ottosen
Contact: nesotto@cs.auc.dk
Organization: Department of Computer Science, Aalborg University, and Dezide Aps
Date: 10th of September 2004
Number:WG21/N1669 and J16/04-0109. This proposal is a revision of paper n1613.
Working Group:Evolution
Copyright: Thorsten Ottosen 2004. All rights reserved

Abstract

Contract Programming 1 is about providing the programmer with stronger tools for expressing correctness arguments directly in the source code. This proposal describes a small assertion sub-language that unifies compile-time and run-time assertions. The benefits are among others a higher degree of self-documenting source code, better design tools, and easier debugging and testing.

Table of Contents

1   Motivation

Language support for Contract Programming has several benefits:

  1. it can remove the need for separation of documentation and implementation (see factorial_example.hpp)
  2. it can make debugging and testing much easier
  3. it can improve communication between designers and programmers in large C++ projects
  4. it can enable the compiler to generate faster code (see restrict_replacement_example.hpp)
  5. it can make inheritance easier to use correctly (see subcontracting_example.hpp )
  6. it can ensure that every programmer understands the contract metaphors 2
  7. it might make static analysis tools much more powerful

Please refer to n1613 for an extensive discussion of these benefits.

Already with the current proposal, it is quite remarkable how much of an interface that can be documented. For a good example, please see how std::vector is declared in vector_example.hpp; there is only a small portion of the specification of std::vector that cannot be described in the contracts.

2   The proposal

The idea is to extend C++

These new contract scopes can contain assertions that may be evaluated either at compiler-time or at run-time as part of the program to verify their correctness.

2.1   Assertions

The basic building blocks of contracts are assertions. Assertions come in two categories:

2.1.1   Static assertions

There are two flavors of static assertions:

  1. default assertions

    syntax:

    static constant-expression : string-literal ;

    example:

    static is_pod<T>::value : "T must model a POD";

  2. select assertions

    syntax:
    1. if( constant-expression ) static-assertion
    2. if( constant-expression ) static-assertion else static-assertion
    example:
    if( is_pod<T>::value )

    static sizeof( T ) <= sizeof( long ) : "Only PODs smaller than long supported";

The static assertions are exactly like the ones described in n1617. The main difference is that we

  1. reuse the keyword static instead of adding a new one,
  2. confine the scope of the static assertion to contract scope, and
  3. allow compile-time select statements to avoid duplication of conditions.

2.1.2   Runtime assertions

There are three flavors of runtime assertions:

  1. default assertions

    syntax:

    boolean-expression ;

    example:

    std::cout.good();

  2. compound assertions

    syntax:

    boolean-expression : expression ;

    example:

    std::cout.good() : terminate();

  3. select assertions

    syntax:
    1. if( condition ) runtime-assertion
    2. if( condition ) runtime-assertion else runtime-assertion
    example:
    if( empty() )

    result == end();

We shall call the left hand side of a compound assertion the condition and the right hand side the action. The following general points are worth noting:

  1. Default assertions defaults to calling terminate(), but the behavior can be customized.
  1. The select assertions remove the need for the implication operator that was discussed in n1613.

  2. The syntactic freedom have been kept minimal to ensure a good documentation effect (see also Allow more statements in contracts).

  3. Every visible variable or parameter is considered const within the scope of contracts (even mutable variables).

  4. Every function call within the assertions must be either

    1. a const member function with no non-const reference or pointer arguments
    2. a free-standing function with no non-const reference or pointer arguments
    3. if the return value is a non-const reference or pointer, it must not be used in any context that would not allow a const qualified reference or pointer

    (see also Allow mutable functions in contracts.)

  5. Function calls within assertions do not check assertions; this is to prevent infinite recursion and to provide reasonable performance (as seen in the factorial_example.hpp).

  6. Throwing an exception is sometimes convenient; bounds-checking is a good example (see also how it is done in vector_example.hpp ).

  7. If the compiler can determine that the condition of an assertion is true, it may choose not to evaluate that assertion.

  8. If the compiler can determine that the condition of an assertion is false, it may choose to call the broken contract handler or call the action without evaluating that condition.

  1. Compound assertions can never be removed by the compiler unless the compiler can prove that the condition is true or unless the action has no effect 3.

The last rule opens up the door for other types of contracts where we can use the comma-operator as seen in the pointer_container_replace_example.hpp.

2.2   Function std::old()

It is very useful to be able to take a copy of a variable to compare it with other values later. In particular, this is true in function postconditions and in loop invariants. These two contract scopes are also the only scopes where std::old() is allowed to appear.

The function can be said to have the following pseudo-declaration:

namespace std
{
    template< class T >
    const T& old( const T& r )
        precondition 
        {
            static is_copy_constructible<T>::value : "old() requires the type to be Copy Constructible";
        }
}

The function must return a reference to a temporary variable. Assume i is a visible int, then the compiler translates

{
    std::old( i ) == 42;
}

into

{
    const int __old_i( i );
    __old_i == 42;
}

A set of rules govern how std::old() behaves within a certain contract:

  1. if it is applied to the same expression n times, that expression is only evaluated once and there only exists one copy of the expression,

  2. the copy of its argument is taken

    1. after the precondition is evaluated if std::old() appears in function postconditions,
    2. before each loop iteration if std::old() appears in loop invariants.

The precondition should be evaluated first to allow it to report its errors first. Notice that we can only apply std::old() to objects of a type that defines a copy-constructor taking a const reference (ie., std::auto_ptr cannot be used).

2.3   Function pre- and postconditions

The function declaration and definition are changed into:

  1. function-declaration1 : function-head
  2. function-declaration2 : function-head function-contract
  3. function-definition1 : function-declaration1 { function-body }
  4. function-definition2 : function-declaration2 do { function-body }
  5. function-contract : precondition-contractopt postcondition-contractopt
  6. precondition-contract : precondition { assertion-sequence }
  7. postcondition-contract : postcondition return-value-declarationopt { assertion-sequence }
  8. return-value-declaration: ( identifier )

example:

double sqrt( double r )
    precondition
    {
        r > 0.;
    }
    postcondition( result )
    {
        equal_within_precision( result * result, r );
    }

In the return-value-declaration we declare a local variable that acts as a const reference to the computed return value. It follows that a return-value-declaration is illegal if the return type is void.

The following general rules apply:

  1. If a function has both a declaration and a definition, the contracts must appear on the declaration.

  2. The execution of a function is now

    1. evaluate the precondition assertion by assertion in order starting from the top,
    2. evaluate std::old() occurrences in the postcondition,
    3. evaluate the function body,
    4. evaluate the postcondition assertion by assertion in order starting from the top.
  1. The execution of a member function is now as in 2, but

    1. 2.a is preceded by a call to the class invariant,

    2. 2.d is preceded by a call to the class invariant,

      • rationale: the contracts might call public functions in the class which require the invariant to be established.
(See also when the class invariant is disabled.)

2.3.1   Virtual functions

If the function F is virtual, we must require that

  1. only the first declaration/definition of F can have a precondition,
  2. if subsequent declarations/definitions of F in derived classes provide a precondition anyway, it results in a compile time error.

Section 3.5 of n1613 explains how little redefinition of preconditions is used. Even though subcontracting is theoretically sound, it ends up being useless in practice since the user cannot take advantage of the weaker precondition by performing a downcast 4. Also, the derived class can provide a separate function with a weaker precondition or the precondition can be specified via a virtual function.

Postconditions can be made stronger in a derived class as seen in the subcontracting_example.hpp. We can summarize the remaining rules for virtual functions as

  1. pure virtual functions can have contracts
  2. postconditions from a function in a base class and the overridden version in a derived class are ANDed together

The last rule ensures that the function in the derived class has a stronger postcondition by design. A programmer can via a downcast obtain the stronger guarantee, but the runtime check must still follow rule 4 above.

2.3.2   Constructors

Constructors behaves much like member functions. This means that a constructor

  1. can have a precondition and a postcondition,
  2. disables the class invariant when calling public functions
  3. calls the class invariant before the postcondition

The differences are that a constructor:

  1. does not evaluate the class invariant before the precondition,
  2. has special rules for evaluating invariants of base-classes (see class invariants).

2.3.3   Destructors

Destructors cannot have preconditions and postconditions. The class invariant, however, is executed before the destructor body. Notice that the rules for evaluating the class invariant ensures that exceptions thrown during evaluation of the class invariant cannot escape.

2.4   Class invariants

Within class scope it is possible to define a class invariant:

syntax:
invariant { assertion-sequence }
example:
see vector_example.hpp

The class invariant has the following properties:

  1. It must appear in the declaration of a class.

  2. It is inherited in the sense that the invariant of a derived class implicitly will have the super-class invariant ANDed to it (see also item 6-7).

    example:

    struct base { invariant { ... } };
    struct derived : base
    {
        invariant
        {
            base::invariant(); // implicitly generated
            ...
        }
    };
    

    (Remark: the above is pseudo-code and is not affected by the disabling of assertions within assertions.)

  3. It can always be called from within or outside the class as if it was a member function with the declaration void invariant() const;.

  4. It is called implicitly from public

    1. pre- and postconditions,
    1. constructors,
    1. destructors,
    1. member functions that exit abnormally via an exception 5
  5. It is always called as if surrounded by a try-catch block:

    try
    {
        class_invariant();
    }
    catch( ... )
    {
        std::class_invariant_broken();
    }
    
  • rationale: this ensures that exceptions thrown in the invariant cannot escape from functions and in particular not from the destructor. 6
  1. For its execution during construction 7 holds that:

    1. each assertion is executed in order starting from the top excluding any part inherited,

      • rationale: if we do not exclude inherited parts, those parts would be evaluated multiple times.
  2. For its execution after construction holds that:

    1. each assertion is executed in order starting from the top including any part inherited,
    2. if the class has any sub-classes, then the inherited portion is executed first,
    3. if the class has several sub-classes the order of the classes in the base-clause is followed.
  3. If the body of a public function F1 calls another public member function F2 of the same instance, the invariant is not called implicitly during that call. 8

Section 7.4 of n1613 discusses the last issue in more detail. In general it seems reasonable to enforce invariants across class boundaries, but to allow a class some more latitude internally.

2.5   Loop invariants

This revision introduces loop invariants. Loop invariants make it easier to verify correct loop behavior. The syntax is

loop-invariant: invariant { assertion-sequence }

An example can be found in factorial_example.hpp. The special function std::old() has a particular meaning inside a loop invariant. Assume i is a visible int; then when the compiler sees

invariant
{
    std::old( i ) == i + 2;
}

it is translated into something like

invariant
{
    const int __old_i = i; // this executes before each loop iteration
    __old_i == i + 2;      // this executes after each loop iteration
}

To summarize the rules, we have

  1. std::old() takes its copy before each loop iteration,

  2. the assertions are evaluated after each loop iteration in order starting from the top,

  3. the entire loop-invariant is evaluated as if it was surrounded by a try-catch block:

    try
    {
        loop_invariant();
    }
    catch( ... ) 
    {
        std::loop_invariant_broken();
    }
    
  4. variables that have a greater scope than the loop are visible in the loop-invariant and std::old() can be applied to them,

  5. loop-variables declared in the loop-body are visible in the loop-invariant as well and std::old() can be applied to them. 9

Notice that std::old() is used to specify variant behavior within the loop invariant---something that usually requires another keyword.

2.5.1   for-loop

syntax:

for ( for-init-statement ; conditionopt ; expressionopt ) statement loop-invariantopt

example:

for( int i = 0; i != 10; ++i )
{
    std::cout << i;
}
invariant
{
   i >= 1 && i <= 10;
   i == std::old( i ) + 1; 
}

2.5.2   while-loop

syntax:

while ( condition ) statement loop-invariantopt

example:

int i = 0;
while( i != 10 )
{
    std::cout << i;
    ++i;
}
invariant 
{
    i >= 1 && i <= 10;
    i == std::old( i ) + 1;
}

2.5.3   do-while-loop

syntax:

do statement loop-invariantopt while ( expression ) ;

example:

int i = 0;
do
{
    std::cout << i;
    ++i;
}
invariant
{
    i >= 1 && i <= 10;
    i == std::old( i ) + 1;
}
while( i != 10 );

2.6   Namespace invariants

To better support global state or namespace state this revision introduces namespace invariants:

syntax:
namespace-invariant: invariant { assertion-sequence }

example:

namespace foo
{
    int     buffer_size;
    int*    buffer;

    invariant
    {
        static  sizeof( int ) >= 4 : "int must be 32 bit"; 
        buffer_size > 0;
        buffer     != 0;
    }
}

The properties of namespace invariants are:

  1. they can appear multiple times in the same namespace across multiple translation units,

  2. for each translation unit, the present invariants are executed once after the static initialization phase, that is, conceptually as the last part of the static initialization phase,

  3. they are always called as if surrounded by a try-catch block:

    try
    {
        namespace_invariant();
    }
    catch( ... )
    {
        std::namespace_invariant_broken();
    }
    
  4. the order of evaluation of the invariants is unspecified,

  5. the order of evaluation of the assertions in an invariant is from top to bottom,

  6. for any namespace N, N::invariant() executes all invariants from namespace N.

2.7   Failure handler functions

The default behavior for all default assertions is to call terminate() via a call to their respective handler. As seen below, we have a handler for each type of contract. If the default behavior is undesirable, the standard library provides the following handlers:

namespace std
{        
    void precondition_broken();
    void postcondition_broken();
    void class_invariant_broken();
    void loop_invariant_broken();
    void namespace_invariant_broken();
    
    typedef void (*broken_contract_handler)();
    
    broken_contract_handler  set_precondition_broken_handler( broken_contract_handler r ) throw();
    broken_contract_handler  set_postcondition_broken_handler( broken_contract_handler r ) throw();
    broken_contract_handler  set_class_invariant_broken_handler( broken_contract_handler r ) throw();
    broken_contract_handler  set_loop_invariant_broken_handler( broken_contract_handler r ) throw();
    broken_contract_handler  set_namespace_invariant_broken_handler( broken_contract_handler r ) throw();
}

This should provide plenty of room for customization. The precondition for all the set_XX_handler functions should be r != 0.

3   Open issues

3.1   Allow more statements in contracts

The only control structure that this proposal allows inside contracts is an if-statement. The questions are then

  1. why not allow all forms of control structures?

    example:

    {
        for( size_type i = 0; i != size(); ++i )
            *this[i] == T();
    } 
    
  2. why not just treat a contract block as any normal C++ block?

For the first question we can observe that

pros:

  1. one can avoid calling a function that embeds the control structure

cons:

  1. more complex specification
  2. a reduced documentation effect since the abstraction level is lowered

If we make a contract block a normal C++ block, we make problem 2 above worse. In addition we must ask

cons:

  1. how should the compiler know what constitutes a run-time assertion?
  2. how should the compiler know what constitutes a static assertion?

The obvious answer to the last question is to add a new special keyword as proposed in n1617.

3.2   Allow mutable functions in contracts

The current proposal prohibits side-effects as much as possible. Otherwise we could end up with different run-time behavior depending on whether or not an assertion is executed. Because C++ knows about constness, C++ really shines in this regard compared to other languages.

So the question is

  • should we allow mutable functions in contracts?

If we were to provide a little more latitude, there could be at least two different ways to reuse mutable:

  1. make the whole block mutable:

    void X::foo( int i )
    precondition mutable
    {
        ...
    }
    
  2. make individual assertions mutable:

    void X::foo( int i )
    precondition
    {
        mutable foo( i );
    }
    

3.3   How do contracts interact with function-try-blocks?

There seems to be at least two solutions:

  1. Forbid function-try-blocks and contracts on the same function.

  2. Allow it as in this example:

    void foo( int i )
        precondition
        {
            i > 0;
        }
        try
        {
            // ...
        }
        catch( ... )
        {
        }
    

In case of 2, then the question would be

  • should the try-block catch exceptions from the pre- and postcondition?

3.4   Should we allow templated contracts?

Pavel Vozenilek asks why contracts cannot be templated. Examples could be

template< class T >
class Foo
{
    invariant<T*> // partial specialization of invariant
    {
       // ...
    }
    
    invariant // default invariant here
    {
       // ...
    }
};    
    
template< class T >
void foo( T r )
    precondition<double>
    { /* only allow full specialization for functions */ }
    precondition
    { /* default */ }

3.5   Are failure handler functions wrongly specified?

Currently a failure handler function does not allow one to

  1. see the context of the broken assertion, or
  2. use other functions than free-standing functions.

It might be desirable to change the functions to

namespace std
{
    class assertion_context
    {
        contract_context( const char* where, const char* assertion ) throw();
        ~contract_context() throw();
        const char* context() const throw();
    };

    void precondition_broken( const assertion_context& cc );
    // ... etc
}

or even

namespace std
{
    extern std::function< void ( const assertion_context& ) > precondition_broken;
    // ... etc
}

This would hopefully ensure good error-messages.

3.6   Do not make invariant a keyword

It could be considered that any static function

void invariant();

and any member function

void X::invariant() const;

automatically defines a namespace invariant and a class invariant, respectively. This would have the following consequences:

pros:

  1. it saves a keyword,

cons:

  1. it could change the behavior of those programs that already defines an invariant,
  2. it would make the syntax and semantics of invariant contracts different from pre- and postcondition contracts.

It might also be worth considering a --no_invariant_keyword compiler option for backward compatibility instead.

4   Major changes from n1613

  1. added loop invariants

  2. added namespace invariants

  3. added static assertions

  4. changed use of keywords:

    before

    now

    in

    precondition

    out

    postcondition

    return

    a local variable

    implies

    if

    in

    std::old()

  5. simplified subcontracting: now preconditions cannot be weakened

5   List of proposals that could be affected by this proposal

  1. static assertions as described in n1617
  2. concepts as described in n1510, n1522 and n1536
  3. any proposal that seeks to enhance meta-programming capabilities

6   List of features that would make Contract Programming stronger

This section describes some crazy ideas that might serve as a basis for further discussion.

6.1   More compiler magic

For the purpose of static analysis either by the compiler or a special tool, it might be convenient to be able to indicate certain functions were invalid for a period of time.

For example, calling operator*() on an iterator could be invalid, yet we cannot explain that to the compiler.

Imagine a magic function std::invalid_operation():

iterator end()
    postcondition( result )
    {
        //
        // expression style
        //
        std::invalid_operation( *result, ++result, result++ );
        
        //
        // function style
        //
        std::invalid_operation( operator*(), operator++(), operator+() );
    }

These operations would then be invalid until a new member function was called that did not have the same invalid operation. For example

iterator i = container.end();
--i;                  // now the operations becomes valid
*i         = a_value; // ok
++i;                  // ok 

A compiler could choose to either

  1. treat the function as documentation only by doing a syntax check, or
  2. see if it can deduce a compile-time error too.

6.2   Changing exception specifications

C++'s exception specifications are not used very much in practice. This is unfortunate since documenting what exceptions (if any) a function throws is important.

In other words, the exception specification seems to be an important part of a functions contract. This proposal already checks the basic guarantee of exception-safety (by checking invariants), and we can already check the strong guarantee in a post-condition:

postcondition
{
   *this == std::old( *this );
}

But there seem two other important cases as well:

  1. the nothrow exception-safety guarantee
  2. a guarantee somewhere between the basic and the strong exception-safety guarantee in case an exception is thrown

So what if we changed the rules for

iterator begin() throw();

to mean

  1. this function promises not to throw exceptions and the compiler can assume that when optimizing
  2. if it does, the behavior is undefined

? If that were the case, throw() would be used much more.

The second situation is when a function exits via an exception, but we still want to guarantee more than the basic guarantee. Imagine that we could do something like this:

postcondition
{
    if( throws( std::exception ) )
    {
       std::old( foo ) == foo; // this variable has not changed
       std::old( bar ) != bar; // but this one has
    }
}

This might provide a way to make stronger assertions in the presence of exceptions.

6.3   Allow test of any precondition

Alf Steinbach suggests that preconditions should be checkable without calling the function:

void foo( ... ) 
    precondition { ... }

// ... 
      
if( foo.precondition( ... ) ) 
   foo( ... )
else
   report_error();   

7   Implementability

Walter Bright has extensive experience from implementing Contract Programming in the C++ and D compilers from Digital Mars. He asserts that it will take about one man month to implement this proposal.

8   List of examples

8.1   vector_example.hpp

///////////////////////////////////////
// Tools
///////////////////////////////////////

template< class Iter, class T >
bool all_equals( Iter first, Iter last, const T& val )
{ /* for simplicity, let us assume T's can be compared */ }

template< class Iter, class Size >
bool equal_distance( Iter first, Iter last, Size size )
{ /* internal tagging mechnism so even input iterators can be passed */ }

///////////////////////////////////////
// New vector interface
///////////////////////////////////////

template< class T, class Alloc = allocator<T> >
class vector 
{
    invariant
    {
        ( size() == 0 ) == empty();
        size() == std::distance( begin(), end() );
        size() == std::distance( rbegin(), rend() );
        size() <= capacity();
        capacity() <= max_size();
        
        static is_assignable<T>::value         : "value_type must be Assignable" ;
        static is_copy_constructible<T>::value : "value_type must be CopyConstructible" ;
    }
    
public:
    typedef Alloc                             allocator_type;
    typedef typename Alloc::pointer           pointer;
    typedef typename Alloc::const_pointer     const_pointer;
    typedef typename Alloc::reference         reference;
    typedef typename Alloc::const_reference   const_reference;
    typedef typename Alloc::value_type        value_type;
    typedef ...                               iterator;
    typedef ...                               const_iterator;
    typedef ...                               size_type;
    typedef ...                               difference_type;
    typedef reverse_iterator<iterator>        reverse_iterator;
    typedef reverse_iterator<const_iterator>  const_reverse_iterator;

             vector()                  
                 postcondition { empty(); } 
                 
    explicit vector( const Alloc& al ) 
                 postcondition { empty(); 
                                 al == get_allocator(); }
                 
    explicit vector( size_type count ) 
                 postcondition { size() == count; 
                                 all_equals( begin(), end(), T() ); }
                 
             vector( size_type count, const T& val ) 
                 postcondition { size() == count; 
                                 all_equals( begin(), end(), val ); }
             
             vector( size_type count, const T& val, const Alloc& al ) 
                 postcondition { size == count; 
                                 all_equals( begin(), end(), val ); 
                                 al == get_allocator(); }:
             
             vector( const vector& right ) 
                 postcondition { right == *this; }
    
             template< class InIt >
             vector( InIt first, InIt last ) 
                 precondition  { static is_input_iterator<InIt>::value : "Iterator argument must model an InputIterator"; }
                 postcondition { equal_distance( first, last, size() ); }
                 
             template< class InIt >
             vector( InIt first, InIt last, const Alloc& al );
                 precondition  { static is_input_iterator<InIt>::value : "Iterator argument must model an InputIterator"; }
                 postcondition { equal_distance( first, last, size() ); 
                                 al = get_allocator(); }

             void reserve( size_type count ) 
                 precondition { count < max_size() : throw length_error(); }
                 postcondition { capacity() >= count; }
                 
             size_type capacity() const;
                 postcondition( result ) { result >= size(); }
                 
             iterator begin()
                 postcondition( result ) { if( empty() ) result == end(); }
             
             const_iterator begin() const
                 postcondition( result ) { if( empty() ) result == end(); }
             
             iterator end();
             const_iterator end() const;
             
             reverse_iterator rbegin()
                 postcondition( result ) { if( empty() ) result == rend(); }
             
             const_reverse_iterator rbegin() const
                 postcondition( result ) { if( empty() ) result == rend(); }
             
             reverse_iterator rend();
             const_reverse_iterator rend() const;
             
             void resize( size_type newsize )
                 postcondition // version 1: with an if
                 { 
                     size() == newsize; 
                     if( newsize > std::old(size()) )
                         all_equals( begin() + std::old(size()), end(), T() );
                 }
             
             void resize( size_type newsize, T val )
                 postcondition // version 2: with ternary operator
                 {
                     size() == newsize; 
                     newsize > std::old(size()) ? 
                         all_equals( begin() + std::old(size()), end(), val ) : true;
                 }
         
             size_type size() const
                 postcondition( result ) { result <= capacity(); }
                 
             size_type max_size() const
                 postcondition( result ) { result >= capacity(); }
             
             bool empty() const
                 postcondition( result ) { result == ( size() == 0 ); }
             
             Alloc get_allocator() const;
             
             reference at( size_type off );
                 precondition { off < size() : throw out_of_range(); }
             
             const_reference at( size_type off ) const;
                 precondition { off < size() : throw out_of_range(); }
                 
             reference operator[]( size_type off )
                 precondition { off < size(); }

             const_reference operator[]( size_type off )
                 precondition { off < size(); }
    
             reference front();
                 precondition { not empty(); }
             
             const_reference front() const;
                 precondition { not empty(); }
    
             reference back()
                 precondition { not empty(); }
             
             const_reference back() const;
                 precondition { not empty(); }
                 
             void push_back( const T& val )
                 precondition  { size() < max_size(); }
                 postcondition { back() == val; 
                                 size() == std::old(size()) + 1; 
                                 capacity() <= std::old(capacity()); }
                 
             void pop_back()
                 precondition  { not empty(); }
                 postcondition { size() == std::old(size()) - 1; }
             
             template< class InIt >
             void assign( InIt first, InIt last )
                 precondition  
                 {
                     static is_input_iterator<InIt>::value : "Iterator argument must model an InputIterator"; 
                     "The range [first,last) is not a sub-range of [begin(),end())";
                 }
                 postcondition { equal_distance( first, last, size() ); }
             
             void assign( size_type count, const T& val )
                 precondition  { count <= max_size(); }
                 postcondition { all_equals( begin(), end(), val ); }
                 
             iterator insert( iterator where, const T& val )
                 precondition  { size() < max_size(); }
                 postcondition( result ) 
                 {
                     *result == val;
                     size()  == std::old(size()) + 1;
                     capacity() >= std::old(capacity());
                     
                     if( capacity() > std::old(capacity()) )
                         "All iterators have been invalidated";
                     else
                         "All iterators in the range [where,end()) have been invalidated";
                 }
             
             void insert( iterator where, size_type count, const T& val )
                 precondition  { size() + count <= max_size(); }
                 postcondition 
                 {
                     size() == std::old(size()) + count;
                     capacity() >= std::old(capacity());
                     
                     if( capacity() == std::old(capacity()) )
                     {
                         all_equals( std::old(prior(where)), std::old(prior(where)) + count, val );
                         "All iterators in the range [where,end()) have been invalidated";
                     }
                     else
                         "All iterators have been invalidated";
                 }
                 
             template< class InIt >
             void insert( iterator where, InIt first, InIt last )
                 precondition  
                 { 
                     static is_input_iterator<InIt>::value : "Iterator argument must model an InputIterator";
                     "The range [first,last) is not a sub-range of [begin(),end())";
                     size() + count <= max_size(); 
                 }
                 postcondition
                 {
                     size() == std::old(size()) + count;
                     capacity() >= std::old(capacity());
        
                     if( capacity() == std::old(capacity()) )
                     {
                         all_equals( std::old(prior(where)), std::old(prior(where)) + count, val );
                         "All iterators in the range [where,end()) have been invalidated";
                     }
                     else
                         "All iterators have been invalidated";
                 }

             iterator erase( iterator where );
                 precondition  
                 { 
                     not empty(); 
                     where != end();
                 }
                 postcondition( result ) 
                 {
                      size() == std::old(size()) - 1; 
                      if( empty() )
                          result == end();
                      "All iterators in the range [where,end()) have been invalidated";
                 }
                 
             iterator erase( iterator first, iterator last )
                 precondition  { size() >= std::distance( first, last ); }
                 postcondition( result ) 
                 {
                      size() == std::old(size()) - std::distance( first, last ); 
                      if( empty() )
                          result == end();
                      "All iterators in the range [first,end()) have been invalidated";
                 }

             void clear();
                 postcondition { empty(); }
                 
             void swap( vector& right )
                 postcondition 
                 { 
                     std::old( *this ) == right;
                     std::old( right ) == *this;
                 }
             
}; // class 'vector'

8.2   factorial_example.hpp

//
// This example shows how Contract Programming removes duplicate
// knowledge because it can turn comments into code.
//
// It also shows a very interesting way of checking that 
// the function's postcondition holds: the implementation
// uses iteration, but the postcondition uses recursion
// to verify the return value.
//
// remark: there is no deep/infinite recursion because
//         contracts are not checked while evaluating
//         a contract. 
//

///////////////////////////////////////////////////////////
// Ordinary form of documentation
///////////////////////////////////////////////////////////

//! Factorial algorithm
/*!

   \pre 'n >= 0'
   \post returns '1' if 'n == 0'
         returns 'factorial(n-1)*n' otherwise
*/
          
template< class T >
inline T factorial( T n )
{
    BOOST_ASSERT( n >= 0 );

    if( n == 0 )
        return 1;
    
    T result     = n;
    T old_result = result;
    for( --n; n != 0; --n )
    {
        result *= n;
        BOOST_ASSERT( n > 0 );
        BOOST_ASSERT( result > old_result && "integer has wrapped around" );
        old_result = result;
    }
    
    return result;
}

///////////////////////////////////////////////////////////
// Contract Programming-style documentation
///////////////////////////////////////////////////////////

template< class T >
inline T factorial( T n )
precondition 
{
    n >= 0; 
}
postcondition( result )
{
    if( n == 0 )
        result == 1;
    else
        result == n * factorial(n-1);
}
do
{
    if( n == 0 )
        return 1;
    
    T result = n;
    for( --n; n != 0; --n )
        result *= n;
    invariant
    {
        n >= 0;
        result > std::old( result ) && "integer has wrapped around"; 
    }
    
    return result;
}

8.3   restrict_replacement_example.hpp

//
// This example shows how Contract Programming can
// provide all the functionality of the 'restrict'
// keyword. Moreover, it will work for iterators that
// are not just pointers.
//
// Caveat: The iterators of eg. std::deque are random-access, but will
//         still work erroneously with this example.
//

namespace std
{
    template< class RandomAccessIterator 
    bool arrays_dont_overlap( RandomAccessIterator first, RandomAccessIterator last,
                              RandomAccessIterator first2, RandomAccessIterator last2 )
    {
        return std::less< typename iterator_value<T>::type* >( &*prior(last), &*first2 ) ||
               std::less< typename iterator_value<T>::type* >( &*prior(last2), &*first );
    }
    
    
    
    template< class RandomAccessIterator >
    void fast_copy( RandomAccessIterator first, RandomAccessIterator last,
                    RandomAccessIterator out )
    precondition
    {
        static is_pod< typename iterator_value<RandomAccessIterator>::type >::value : "Only PODs can be copied";
        static is_random_access_iterator<RandomAccessIterator>::value : "The iterator must model a Random Access Iterator";
        arrays_dont_overlap( first, last, out, out + std::distance(first,last) );  
    }
    do
    {
        memcpy( &*out, &*first, std::distance(first,last) );
    }
}

8.4   subcontracting_example.hpp

//
// This example shows how Contract Programming 
// allows one to keep the virtual function public 
// and still enforce the contract of the function
//

class shape
{
public:
    virtual ~shape() {}
    
    virtual int compute_area() const = 0
        postcondition( result ) 
        {
            result > 0;
        }
};

class circle : public shape
{
public:
    int radius() const;
    
    virtual int compute_area() const
        postcondition( result )
        {
            result == pi * radius() * radius();
        }
};

8.5   pointer_container_replace_example.hpp

//
// This example shows how we can perform
// a clean-up action as a side-effect in a precondition.
//
// Side-effects are normally banned from contracts, but in this
// we do it to obhold exception-safety requirements.
//

template< class T >
class ptr_vector
{
public:
    // ...
      
    void replace( T* p, size_type where )
        precondition
        {
            p != 0          : throw bad_ptr();
            where < size(); : delete p, throw bad_index();
        }
};

9   Comparison of Contract Programming in D, Eiffel and C++

The table below contains a comparison of how Contract Programming is implemented in D, Eiffel and C++.

Feature ISE Eiffel 5.4 D C++ Proposal
keywords require, ensure, do, require else, ensure then, invariant, old, result, variant in, out, body, invariant, assert, static precondition, postcondition, do, invariant, static
on failure throws exception throws exception defaults to terminate(), defaults can be customized, might throw
expression copying in postconditions yes, old keyword no yes, std::old() function
subcontracting yes yes yes, but only considers postconditions
contracts on abstract functions yes no yes
arbitrary code contracts yes yes no, must be const correct
function code ordering pre -> body -> post pre -> post -> body pre -> post -> body
compile-time assertions no yes yes
loop invariants yes no yes
loop variants yes no yes, std::old() inside loop invariants
const-correct no no yes
invariant calls
  • end of "constructor"
  • around public functions
  • end of constructor
  • around public functions
  • start of destructor
  • as in D
  • when a function exits due to an exception
disabling of checks during assertions yes no yes
when public func. call public func. disable all checks disable nothing disable invariant
removable from object code yes yes only default assertions

10   Acknowledgements

Special thanks goes to

11   Footnotes

[1]The original term "Design by Contract" is abandoned for good since it appears to have been trademarked in 2003. The term "Contract Programming" was suggested by Walter Bright.
[2]

Even experienced programmers can choke on the word "invariant" and what it means for a class to have one. There are a few simple rules we want all programmers to learn:

  1. that classes can have invariants and that subclasses have stronger or equally strong invariants,
  2. that functions have pre- and postconditions: the implementer has as his obligation to fulfill the postcondition assuming the precondition holds; the user has as his obligation to fulfill the precondition and receives the benefits of the postcondition in return,
  3. that public functions cannot break the class invariant.
[3]

This latitude allows programmers to turn off and on compound assertions using appropriate macros and can be helpful if the more levels of assertions are wanted. For example, an assertion like

is_foo() : (void)0;

can be discarded.

[4]

Assume we want to take advantage of a weaker precondition. Normally that precondition is weaker by design, that is, the two preconditions are ORed no matter what they contain. Even if we perform a downcast, the runtime system must call first the original contract (which will then fail). Then the control is handled to the derived precondition which can then fail or not. This seems extremely messy and might require try-catch block around the first precondition.

The alternative is to only check the derived precondition if we have performed a downcast. The consequence is that we might have a precondition that is in fact stronger than the original! In general it is probably also impossible to verify that a contract is weaker given that it can contain arbitrary expressions. This approach does not seem very attractive either.

If we also take into consideration that good examples with weakened preconditions are extremely rare, it is be better to abandon the idea all together.

Thanks goes to Scott Meyers and Attila Fehér for their input on this issue.

[5]To ensure that the function gives the basic guarantee of exception-safety.
[6]One can imagine an approach where exceptions could escape from an invariant by not checking invariants when functions exit via an exception. The benefits of such an approach are not obvious and it will complicate flow analysis unnecessarily.
[7]During construction means until the post-condition of the constructor has ended.
[8]An implementation would not be required to detect when control leaves a class in general but merely to disable invariants until the function returns. This means that if A::foo() calls B::foo() which calls A::bar(), then the invariant of A will not be checked on entry to or exit of A::bar(). However, B::foo() may choose to check the invariant of A manually.
[9]This is contrary to the loop condition which cannot see these variables.