2.1   Assertions

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

• static assertions

• runtime assertions

2.2   Keyword __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.

Assume i is a visible int, then the compiler translates

{
    __old i == 42;
}

into

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

A set of rules govern how __old 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.

The precondition should be evaluated first to allow it to report its errors first. Notice that we can only apply __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. 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 __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.

2.4   Class invariants

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

syntax:

1. static-class-invariant : static invariant { static-assertion-sequence }
2. runtime-class-invariant : invariant { runtime-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.)

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. member functions' 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 [10]

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

6. For its execution during construction [12] 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.

2.5   Namespace invariants

To better support global state or namespace state we introduces namespace invariants:

syntax:

1. static-namespace-invariant: static invariant { static-assertion-sequence }
2. runtime-namespace-invariant: invariant { runtime-assertion-sequence }

example:

namespace foo
{
    int     buffer_size;
    int*    buffer;

    invariant
    {
        buffer_size > 0;
        buffer     != 0;
    }

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

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

3.1   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.2   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.3   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.

Another possibility is to require certain contracts (in particular preconditions) to be used in the standard library. This might be a way for the committee to guarantee a safer version of the standard library to novices.

7.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 
{
    static invariant
    {
        static is_assignable<T>::value         : "value_type must be Assignable" ;
        static is_copy_constructible<T>::value : "value_type must be CopyConstructible" ;
    }
    
    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 ) 
                 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(); }
                 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 > __old size() )
                         all_equals( begin() + __old size(), end(), T() );
                 }
             
             void resize( size_type newsize, T val )
                 postcondition // version 2: with ternary operator
                 {
                     size() == newsize; 
                     newsize > __oldsize()) ? 
                         all_equals( begin() + __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(); }
             
             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() == __old size() + 1; 
                                 capacity() >= __old capacity(); }
                 
             void pop_back()
                 precondition  { not empty(); }
                 postcondition { size() == __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()  == __old size() + 1;
                     capacity() >= __old capacity();
                     
                     if( capacity() > __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() == __old size() + count;
                     capacity() >= __old capacity();
                     
                     if( capacity() == __old capacity() )
                     {
                         all_equals( __old prior(where), __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() == __old size() + count;
                     capacity() >= __old capacity();
        
                     if( capacity() == __old capacity() )
                     {
                         all_equals( __old prior(where), __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() == __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() == __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 
                 { 
                     __old *this == right;
                     __old right == *this;
                 }
             
}; // class 'vector'

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