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

Author: Lawrence Crowl and Thorsten Ottosen
Contact: lawrence.crowl@sun.com and nesotto@cs.aau.dk
Organization: Sun Microsystems and Dezide Aps
Date: 2005-08-24
Number:WG21/N1866 and J16/05-0126. This proposal is a revision of paper n1773.
Working Group:Evolution

Abstract

Contract Programming is about providing the programmer with stronger tools for expressing correctness arguments directly in the source code. Moreover, the contracts enable new and powerful optimization opportunities. 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.
  1. It can enable the compiler to generate faster code [0] (see also Contracts for performance).
  1. It can make debugging and testing much easier.
  1. It can improve communication between designers and programmers in large C++ projects.
  1. It can make inheritance easier to use correctly (see subcontracting_example.hpp ).
  1. It can ensure that every programmer understands the contract metaphors [1] .
  1. It can enable more powerful static analysis tools.

Please refer to n1800 and 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:
    1. static-assertion: constant-expression : string-literal ;
    example:

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

  2. select assertions

    syntax:
    1. static-assertion-sequence:
    2. static-assertion-sequence: static-assertion-sequence static-assertion
    3. static-body: static-assertion
    4. static-body: { static-assertion-sequence }
    5. static-if-assertion : if( constant-expression ) static-body static-else-assertion opt
    6. static-else-assertion : else static-body
    example:
    if( is_pod<T>::value )

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

The contant-expression is implicitly converted to bool.

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

  1. confine the scope of the static assertion to contract scope, and
  1. allow compile-time select statements to avoid duplication of conditions.

2.1.2   Runtime assertions

There are two flavors of runtime assertions:

  1. default assertions

    syntax:
    1. runtime-assertion : boolean-expression importance-ordering opt ;
    2. importance-ordering : : integer-constant
    example:

    std::cout.good();

  2. select assertions

    syntax:
    1. runtime-assertion-sequence :
    2. runtime-assertion-sequence : runtime-assertion-sequence runtime-assertion
    3. runtime-body : runtime-assertion
    4. runtime-body : { runtime-assertion-sequence }
    5. runtime-if-assertion : if( condition ) runtime-body runtime-else-assertion opt
    6. runtime-else-assertion : else runtime-body
    example:
    if( empty() )

    result == end();

The following general points are worth noting:

  1. Default assertions defaults to calling terminate(), but the behavior can be customized.

  2. The select assertions remove the need for the implication operator that was discussed in n1613.

  3. The syntactic freedom has been kept minimal to ensure a good documentation effect.

  4. All visible functions and variables can be used within contract scope.

  5. Member reference within constract scope is subject to the same constraints as member reference within const member functions.

  1. If the compiler can determine that the condition of an assertion is true, it may choose not to evaluate that assertion.
  1. 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. Importance ordering allows users to specify multiple levels of assertions. The higher an integer, the more crucial it is to keep an assertion in the object code.
  1. The default importance ordering is 0 and is in effect when no integer is specified.

It is possible to mix static and runtime assertions. In that case talk about assertion sequences:

  1. assertion-sequence :
  2. assertion-sequence : assertion-sequence static-assertion-sequence
  3. assertion-sequence : assertion-sequence runtime-assertion-sequence

2.2   Function pre- and postconditions

The function declaration and definition are changed into:

  1. precontracted-function : function-head
  2. precontracted-function : function-head precondition-contract
  3. postcontracted-function : precontracted-function
  4. postcontracted-function : precontracted-function postcondition-contract
  5. function-declaration : postcontracted-function ;
  6. function-definition : postcontracted-function { function-body }
  7. precondition-contract : precondition { assertion-sequence }
  8. postcondition-contract : postcondition return-value-declarationopt { assertion-sequence }
  9. 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 oldof occurrences in the postcondition,
    3. evaluate the function body,
    4. evaluate the postcondition assertion by assertion in order starting from the top.
  3. 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.
  4. Function-try-blocks can appear together with pre- and postconditions on function definitions.

  5. Pre- and postconditions are evaluated outside any function-try-block.

  1. During execution of the postcondition other contracts (recursively encountered) are not evaluated.

2.2.1   Virtual functions

If the function F is virtual, we require that

  1. only the first declaration/definition of F can have a precondition.

Section 3.5 of n1613 explains how little redefinition of preconditions is used. Even though subcontracting is theoretically sound, it ends up being fairly useless in practice [3].

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,
  1. postconditions from a function in a base class and the overridden version in a derived class are ANDed together [4].

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 3 above.

In connection with multiple inheritance we require special rules. if F overrides more than one virtual function due to multiple inheritance, it holds that

  1. the precondition on F is an ORing of the preconditions of all the functions F override,
  1. the postcondition on F is an ANDing of (1) the postconditions of all the functions F override and (2) F's own postcondition.

2.2.2   Constructors

Constructors behave much like member functions. This means that a constructor can have a precondition and a postcondition.

2.2.3   Function pointers

If the address of a function is taken, it holds that

  1. the precondition is evaluated before the function body when the function is called through the function pointer.

Remark: A compiler might be able to determine that the precondition is satisfied, in that case the compiler may generate a call directly to the function body (thus sharing implementation with the function pointer call).

2.3   Keyword oldof

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.

Assume i is a visible int, then the compiler translates

{
    oldof i == 42;
}

into

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

A set of rules govern how oldof behaves within a certain contract:

  1. If it is applied to the same expression n times, that expression need only be evaluated once and only one copy need to be stored.
  1. The copy of its argument is taken after the precondition is evaluated.

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

2.4   Class invariants

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

syntax:
  1. class-invariant : 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 base-class invariant(s) 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,

      • call the class invariant before the postcondition,
    2. destructors,

      • call the class invariant before the destructor body.
    3. 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.

2.5   Namespace invariants

To better support assertions at namespace scope or function-scope we use namespace invariants:

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

example:

namespace foo
{
    int     buffer_size;
    int*    buffer;

    invariant
    {
        buffer_size > 0;
        buffer     != 0;
        sizeof( int ) >= 4 : "int must be 32 bit"; 
    }
    
    void foo()
    {
        int i = 0;
        for(;;)
        {
            invariant { i < 10; }
            ...
        }
    }
}

The namespace invariants use the same syntax as the class invariant, but appears in different scopes and is called in different ways.

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(); // pseudo code
    }
    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.6   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 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_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.

2.7   Changes to the standard library

We suggest that no required changes should be made to the standard library. An implementation is free to implement all standard guarantees in terms of contract code, but not required to.

3   Contracts for performance

This section discusses how contracts can help the compiler to generate faster code.

A limited form of contract programming is the use of the assert() macro. Its use is standard practice in many software projects. Unfortunately, it suffers from several problems. We will evaluate these problems by distinguishing between a library and its client.

3.1   assert() is evaluated within the library

As a consequence, the enabling or disabling of assertion checking is a compile-time decision of the library. The result is generally either

  1. no checking, in which case errors are lost, or
  2. checking, in which case performance is lost.

In contrast, preconditions may be evaluated in the client. The client decides on the acceptable tradeoff between performance and checking.

3.2   assert() fails to distinguish between checking arguments and validating computations

In well-tested production code, validating computation is rarely needed, because the function has proven itself. On the other hand, checking arguments has continuing need because of the evolution of callers. With only a single form, programmers that turn off validating computation for performance, will also turn off checking arguments.

In contrast, the proposed syntactic distinction between preconditions, postconditions and invariants preserves the very real need to enable them separately.

3.3   assert() is indistinguishable from regular code

As a consequence it is very difficult for a compiler to make use of the contents of an assert() macro.

In contrast, preconditions, postconditions and invariants are very visible to the compiler. The compiler can use preconditions and postconditions as a constraint on the value-space of the code, which in turn enables optimization.

Explicit preconditions and postconditions enable optimization in two ways.

  1. The compiler can eliminate conditions known statically.

    For example, given

    char *foo()
    postcondition( result ) { result != 0; };
    
    void bar( char *arg )
    precondition { arg != 0; }
    ...
    bar( foo() )
    

    the compiler can propagate the postcondition of foo() to the precondition of bar() and entirely eliminate the precondition checking in bar().

  2. The compiler can use conditions to guide code generation.

    For example, given

    double sum( int count, double array[] )
    precondition { count % 4 == 0; }
    {
        double accum = 0.0;
        for ( int i = 0; i < count; i++ )
                accum += array[i];
        return accum;
    }
    

    the compiler can unroll the loop four times, and avoid generating the stuttering at the start of the loop.

    Furthermore, given the same code but with a precondition of count > 1000, the compiler could chose to implement the loop in parallel. Likewise, with count< 100, the compiler may forgo any checking for the possibility of parallelism.

4   Implementation model for contracts

This section discusses the feasibility of implementation. We provide an implementation model that is reasonable and consistent with the above proposal.

Consider the function

int factorial( int n )
precondition 
{
    0 <= n && n <= 12;
}
postcondition( result ) 
{
    result >= 1;
}
{
    if ( n < 2 )
        return 1;
    else
        return n * factorial( n - 1 );
}

When all conditions are enabled, the compiler generates three functions:

  1. The core function without any condition checking.

    Call this function when compiler switches disable all condition evaluation.

  2. A postcondition evaluator, which calls core function and then executes the postcondition.

    Call this function from normal code when the caller evaluates the preconditions.

  3. A precondition evaluator, which executes the precondition and then calls the postcondition evaluator.

    Call this function when the caller does not or cannot evaluate the preconditions. (Remark: the precondition evaluator would for example be used when a function is called via a function-pointer.)

When postconditions are disabled, a library-build-time decision, the first two functions above are identical, and may be implemented as a single function with two labels.

When preconditions are disabled, a client-build-time decision, the client simply calls the second function.

The evaluation of class invariants is dependent on the evaluation of the preconditions and postconditions that call them. As an additional performance option, compilers can turn of invariant evaluation while still enabling other conditions.

Furthermore, a compiler might choose to provide a switch for generating a single call to the invariant in the constructor.

5   Open issues

5.1   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.

6   Major changes from n1773

  1. reformulated the syntax of static assertions (no use of static keyword).

  2. reformulated the syntax of runtime assertions (we now allow importance ordering).

  3. the invariant mechanisms have been merged (hence now much simpler).

  4. changed use of keyword:

    before

    now

    __old

    oldof

7   List of proposals that could be affected by this proposal

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

8   Implementability

We expect that it will take about 3 man months to implement the proposal without dedicating any time to optimizations.

9   Alternative syntax

In Lillehammer it was suggested to use normal C++ syntax for separation of assertions. In particular it was suggested to write an assertion-sequence as

{
    foo() &&
    bar() &&
    true;
}

instead of

{
    foo();
    bar();
    true;
} 

A full example have been made with the proposed syntax (see vector_example_alternative_syntax.hpp).

It is quite obvious that this syntax has the following drawbacks:

  1. it becomes harder for debuggers to break on individual assertions, because the whole assertion-sequence is a single statement
  1. the ternary operator is harder to read than if-statements
  1. the combination of assertion : "string" and assertion : 2 do not look good.

10   List of examples

10.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
    {
	is_assignable<T>::value         : "value_type must be Assignable" ;
	is_copy_constructible<T>::value : "value_type must be CopyConstructible" ;

        ( size() == 0 ) == empty();
        size() == std::distance( begin(), end() );
        size() == std::distance( rbegin(), rend() );
        size() <= capacity();
        capacity() <= max_size();
    }
    
    
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  { 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  { 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(); }
                 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 > oldof size() )
                         all_equals( begin() + oldof size(), end(), T() );
                 }
             
             void resize( size_type newsize, T val )
                 postcondition // version 2: with ternary operator
                 {
                     size() == newsize; 
                     newsize > oldof size()) ? 
                         all_equals( begin() + oldof 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(); }
             
             const_reference at( size_type off ) const;
                 precondition { off < size(); }
                 
             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() == oldof size() + 1; 
                                 capacity() >= oldof capacity(); }
                 
             void pop_back()
                 precondition  { not empty(); }
                 postcondition { size() == oldof size() - 1; }
             
             template< class InIt >
             void assign( InIt first, InIt last )
                 precondition  
                 {
                     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()  == oldof size() + 1;
                     capacity() >= oldof capacity();
                     
                     if( capacity() > oldof 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() == oldof size() + count;
                     capacity() >= oldof capacity();
                     
                     if( capacity() == oldof capacity() )
                     {
                         all_equals( oldof prior(where), oldof 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  
                 { 
                     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() == oldof size() + count;
                     capacity() >= oldof capacity();
        
                     if( capacity() == oldof capacity() )
                     {
                         all_equals( oldof prior(where), oldof 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() == oldof 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() == oldof 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 
                 { 
                     oldof *this == right;
                     oldof right == *this;
                 }
             
}; // class 'vector'

10.2   vector_example_alternative_syntax.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
    {
	is_assignable<T>::value         : "value_type must be Assignable" &&
	is_copy_constructible<T>::value : "value_type must be CopyConstructible" &&
        ( size() == 0 ) == empty() &&
        size() == std::distance( begin(), end() ) &&
        size() == std::distance( rbegin(), rend() ) &&
        size() <= capacity() &&
        capacity() <= max_size();
    }
    
    
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  { 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  { 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(); }
                 postcondition { capacity() >= count; }
                 
             size_type capacity() const;
                 postcondition( result ) { result >= size(); }
                 
             iterator begin()
                 postcondition( result ) { empty() ? result == end() : true; }
             
             const_iterator begin() const
                 postcondition( result ) { empty() ? result == end() : true; }
             
             iterator end();
             const_iterator end() const;
             
             reverse_iterator rbegin()
                 postcondition( result ) { empty() ? result == rend() : true; }
             
             const_reverse_iterator rbegin() const
                 postcondition( result ) { empty() ? result == rend() : true; }
             
             reverse_iterator rend();
             const_reverse_iterator rend() const;
             
             void resize( size_type newsize )
                 postcondition // version 1: with an if
                 { 
                     size() == newsize &&
                     newsize > oldof size() ?
                         all_equals( begin() + oldof size(), end(), T() ) : true;
                 }
             
             void resize( size_type newsize, T val )
                 postcondition // version 2: with ternary operator
                 {
                     size() == newsize && 
                     newsize > oldof size()) ? 
                         all_equals( begin() + oldof 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(); }
             
             const_reference at( size_type off ) const;
                 precondition { off < size(); }
                 
             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() == oldof size() + 1 && 
                                 capacity() >= oldof capacity(); }
                 
             void pop_back()
                 precondition  { not empty(); }
                 postcondition { size() == oldof size() - 1; }
             
             template< class InIt >
             void assign( InIt first, InIt last )
                 precondition  
                 {
                     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()  == oldof size() + 1 &&
                     capacity() >= oldof capacity() &&
                     
                     capacity() > oldof capacity() ?
                         "All iterators have been invalidated" :
                         "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() == oldof size() + count &&
                     capacity() >= oldof capacity() &&
                     
                     capacity() == oldof capacity() ?
                         all_equals( oldof prior(where), oldof prior(where) + count, val ) &&
                         "All iterators in the range [where,end()) have been invalidated" :
                         "All iterators have been invalidated";
                 }
                 
             template< class InIt >
             void insert( iterator where, InIt first, InIt last )
                 precondition  
                 { 
                     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() == oldof size() + count &&
                     capacity() >= oldof capacity() &&
        
                     capacity() == oldof capacity() ?
                         all_equals( oldof prior(where), oldof prior(where) + count, val ) &&
                         "All iterators in the range [where,end()) have been invalidated":
                         "All iterators have been invalidated";
                 }

             iterator erase( iterator where );
                 precondition  
                 { 
                     not empty() && 
                     where != end();
                 }
                 postcondition( result ) 
                 {
                      size() == oldof size() - 1 &&
						   
                      empty() ? result == end() : true &&
						  
                      "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() == oldof size() - std::distance( first, last ) && 
                      empty() ? result == end() &&
                      "All iterators in the range [first,end()) have been invalidated";
                 }

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

10.3   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();
        }
};

11   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, 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, oldof keyword
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 no
loop variants yes no no
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 no
when public func. call public func. disable all checks disable nothing disable nothing
removable from object code yes yes yes

12   Acknowledgements

The following people has been provided feedback and comments throughout the proposals history: Reece Dunn, Douglas Gregor, Alf Steinbach, Matthew Wilson, Berend de Boer, Darren Cook, Pavel Vozenilek, Scott Meyers, Attila Fehér, Walter Bright, Per Madsen, Kevlin Henney, Sergey Vlasov, Bob Bell, John Nagle, Daveed Vandevoorde, Jaakko Jarvi, Christopher Diggins, John Torjo, Robert Kawulak, Dave Harris, Michael Wong, Thomas Witt, Tim Rowe.

Special thanks goes to David Abrahams and James Widman.

13   Footnotes

[0]For example, if the compiler can determine that a precondition is satisfied, it can call a function where the precondition is not checked. Also, the compiler can always assume contracts to be true; hence the compiler can take advantage of the precondition in the function body.
[1]

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.
[2]A good compiler will emit warnings whenever a mutation is detected within a contract. This is a major advantage compared to the ad hoc solutions programmers use today; there is no special scope and hence no way the compiler can emit those warnings.
[3]A weaker precondition can be taken advantage of if we know the particular type of the object. If weaker preconditions should be allowed, then there exists two alternatives: to allow reuse of an existing contract or to require a complete redefinition. The former favours expressiveness, the latter favours overview.
[4]In some cases the compiler will be able to determine overlapping expression and hence optimize some assertions away.
[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.