4.1   Assertions

The basic building blocks of contracts are assertions.

4.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-declaration_opt { 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 [11].

3. The execution of a member function is now as in 2, but

   1. 2.a is followed by a call to the class invariant [9]

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

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.

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

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

2. The copy of its argument is taken after the precondition is evaluated and before the function body 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).

4.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 is called implicitly from public

   1. pre- and postconditions,

   2. constructors,

      • call the class invariant before the postcondition,

   3. destructors,

      • call the class invariant before the destructor body.

   4. member functions that exit abnormally via an exception [5]

4. 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]

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

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

7. During execution of the invariant other contracts (recursively encountered) are not evaluated.

4.5   block invariants

To better support assertions at block scope we use block invariants:

syntax:

1. block-invariant: invariant { assertion-sequence }

example:

void foo()
{
    int i = 0;
    for(;;)
    {
        invariant { i < 10; }
        ...
    }
}

The block invariants use the same syntax as the class invariant. The properties of block invariants are:

1. they can appear multiple times in the same scope,

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

   try
   {
       block_invariant(); // pseudo code
   }
   catch( ... )
   {
       std::block_invariant_broken();
   }
   

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

4.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 block_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_block_invariant_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.

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

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

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

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

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
    {
        ( 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 ) 
                 postcondition { equal_distance( first, last, size() ); }
                 
             template< class InIt >
             vector( InIt first, InIt last, const Alloc& al );
                 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 {"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  
                 { 
                     "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   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();
        }
};

10.3   recursion example

Consider the relationship between these two comparison operators:

bool operator==( T l, T r )
    postcondition( result )
    {
        result == !( l != r );
    }
        
bool operator!=( T l, T r )
    postcondition( result )
    {
        result == !( l == r );
    }

There is no easy way we can express that using an assert() in the body of the functions.