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

Author: David Abrahams, Lawrence Crowl, Thorsten Ottosen, James Widman
Contact: dave@boost-consulting.com, lawrence.crowl@sun.com, nesotto@cs.aau.dk, widman@gimpel.com
organizations:Boost-Consulting, Sun Microsystems, Dezide Aps, Gimpel Software
Date: 2005-03-04
Number:WG21/N1773 and J16/05-0033. This proposal is a revision of paper n1669.
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 [0].
  1. It can enable the compiler to generate faster code [1].
  1. It can make debugging and testing much easier [2].
  1. It can improve communication between designers and programmers in large C++ projects [3].
  1. It can make inheritance easier to use correctly (see subcontracting_example.hpp ).
  1. It can ensure that every programmer understands the contract metaphors [4] .
  1. It might make static analysis tools much more powerful [5].
  1. It will benefit C++'s image as a secure language [6].

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

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

2   The proposal

The idea is to extend C++

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

2.1   Assertions

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

2.1.1   Static assertions

There are two flavors of static assertions:

  1. default assertions

    syntax:

    static-assertion: static constant-expression : string-literal ;

    example:

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

  2. select assertions

    syntax:
    1. static-assertion-sequence: static-assertion
    2. static-assertion-sequence: static-assertion static-assertion-sequence
    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 )

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

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

  1. reuse the keyword static instead of adding a new one,
  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:

    runtime-assertion : boolean-expression ;

    example:

    std::cout.good();

  2. select assertions

    syntax:
    1. runtime-assertion-sequence : runtime-assertion
    2. runtime-assertion-sequence : runtime-assertion runtime-assertion-sequence
    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 have been kept minimal to ensure a good documentation effect.

  4. Wrt. constness, then contract scope behaves as if it was a const member function [7].

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

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

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

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

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.
  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 __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-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 __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.3.1   Virtual functions

If the function F is virtual, we must require that

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

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

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

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.

2.3.2   Constructors

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

  1. can have a precondition and a postcondition,

2.3.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.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,
    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 [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]
  1. 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.
  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 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   Open issues

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.

4   Major changes from n1669

  1. removed loop invariants

  2. reformulated the syntax of static assertions

  3. reformulated the syntax of runtime assertions

  4. removed rules demanding assertions to be disabled within assertions

  5. removed rules demanding invariants to be disabled within public functions

  6. changed use of keyword:

    before

    now

    std::old()

    __old

5   List of proposals that could affect or 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
  4. reading() specifications as described in n1664

6   Implementability

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

7   List of examples

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

8   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, __old 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

9   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 and Tim Rowe.

10   Footnotes

[0]Today, a lot of redundancy is involved in maintaining documentation and implementation separately. With this proposal a large amount of comments can be made into code ensuring the documentation stays updated and ensuring zero redundancy.
[1]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.
[2]Testing consists mainly of verifying that the functions' contracts are actually fulfilled. With language support for Contract Programming, the contracts are made explicit and hence it becomes easier to see what to test. Furthermore, when testability is hard, the contracts themselves provide an effective runtime test.
[3]Errors often happen when people have to communicate. With language support for Contract Programming there is less need for an informal specification language and hence less room for errors. For example, it should no longer be necessary to translate manually the specifications from the "designer language" to the "programmer language".
[4]

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.
[5]Static analysis tools (the compiler's optimizer included) might be able to start their analysis at a higher level than usual. For example, instead of an analysis of the ins and outs of std::vector<T>, then the tool might start its analysis with the definition of the invariant of std::vector<T>.
[6]Security has been and is a big problem with C (and to a much lesser extend C++) library functions. This insecurity is tightly coupled to the fact that function preconditions are violated and/or that function postconditions are misunderstood. By making the contract aspects of programming more explicit, we can improve the situation.
[7]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.
[8]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.
[9]In some cases the compiler will be able to determine overlapping expression and hence optimize some assertions away.
[10]To ensure that the function gives the basic guarantee of exception-safety.
[11]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.
[12]During construction means until the post-condition of the constructor has ended.