2.1   Assertions

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

• static assertions
• runtime assertions

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-contract_opt postcondition-contract_opt
6. precondition-contract : precondition { assertion-sequence }
7. postcondition-contract : postcondition return-value-declaration_opt { 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.

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.

(See also when the class invariant is disabled.)

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,

   2. constructors,

   3. destructors,

   4. member functions that exit abnormally via an exception ⁵

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. For its execution during construction ⁷ 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.

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

8. 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. ⁸

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

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

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

3. how should the compiler know what constitutes a run-time assertion?
4. 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.

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

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