Extras
This section can be consulted selectively for specific topics of interest.

Old Value Requirements (Templates)
Old values require to copy the expression passed to BOOST_CONTRACT_OLDOF thus the type of that expression needs to be copyable. More precisely, dereferencing an old value pointer of type boost::contract::old_ptr<T> requires boost::contract::is_old_value_copyable<T>::value to be true, otherwise this library will generate a compile-time error.
In some cases it might be acceptable, or even desirable, to cause a compile-time error when a program uses old value types that are not copyable (because it is not possible to fully check the correctness of the program as stated by the contract assertions that use these old values). In these cases, programmers can declare old values using boost::contract::old_ptr as seen so far.
However, in some other cases it might be desirable to simply skip assertions that use old values when the respective old value types are not copyable, without causing compile-time errors. Programmers can do this using boost::contract::old_ptr_if_copyable instead of boost::contract::old_ptr and checking if the old value pointer is not null before dereferencing it in postconditions. For example, consider the following function template that could in general be instantiated for types T that are not copy constructible (that is for which boost::contract::is_old_value_copyable<T>::value is false, see old_if_copyable.cpp): [72]
[72] Rationale: [N1962] and other proposals to add contracts to C++ do not provide a mechanism to selectively disable copies only for old value types that are not copy constructible. However, this library provides such a mechanism to allow to program contracts for template code without necessarily adding extra copy constructible type requirements that would not be present if it were not for copying old values (so compiling the code with and without contracts will not necessarily alter the type requirements of the program). Something similar could be achieved combing C++17 if constexpr with [N1962] or [P0380] so that old value expressions within template code can be guarded by if constexpr statements checking if the old value types are copyable or not. For example, assuming old values are added to [P0380] (using some kind of oldof(...) syntax) and that C++17 if constexpr can be used within [P0380] contracts:

template<typename T>
void offset(T& x, int count)
    [[ensures: if constexpr(std::is_copy_constructible<T>::value) x == oldof(x) + count]]
...

template<typename T> // T might or might not be copyable.
void offset(T& x, int count) {
    // No compiler error if T has no copy constructor...
    boost::contract::old_ptr_if_copyable<T> old_x = BOOST_CONTRACT_OLDOF(x);
    boost::contract::check c = boost::contract::function()
        .postcondition([&] {
            // ...but old value null if T has no copy constructor.
            if(old_x) BOOST_CONTRACT_ASSERT(x == *old_x + count);
        })
    ;

    x += count;
}

The old value pointer old_x is programmed using boost::contract::old_ptr_if_copyable. When T is copyable, boost::contract::old_ptr_if_copyable<T> behaves like boost::contract::old_ptr<T>. When T is not copyable instead, boost::contract::old_ptr_if_copyable<T> will simply not copy x at run-time and leave old_x initialized to a null pointer. Therefore, boost::contract::old_ptr_if_copyable objects like old_x must be checked to be not null as in if(old_x) ... before they are dereferenced in postconditions and exception guarantees (to avoid run-time errors of dereferencing null pointers).
If the above example used boost::contract::old_ptr instead then this library would have generated a compile-time error when offset is instantiated with types T that are not copy constructible (but only if old_x is actually dereferenced somewhere, for example in the contract assertions using *old_x ... or old_x->...). [73]
[73] Technically, on C++17 it is possible to use boost::contract::old_ptr together with if constexpr instead of using boost::contract::old_ptr_if_copyable, for example:

template<typename T>
void offset(T& x, int count) {
    boost::contract::old_ptr<T> old_x;
    if constexpr(boost::contract::is_old_value_copyable<T>::value) old_x = BOOST_CONTRACT_OLDOF(x);
    boost::contract::check c = boost::contract::function()
        .postcondition([&] {
            if constexpr(boost::contract::is_old_value_copyable<T>::value) BOOST_CONTRACT_ASSERT(x == *old_x + count);
        })
    ;

    x += count;
}

However, the authors find this code less readable and more verbose than its equivalent that uses boost::contract::old_ptr_if_copyable. Guarding old value copies and related assertions with if constexpr is useful instead when the guard condition checks type requirements more complex than just boost::contract::is_old_value_copyable (as shown later in this documentation).
When C++11 auto declarations are used with BOOST_CONTRACT_OLDOF, this library always defaults to using the boost::contract::old_ptr type (because its type requirements are more stringent than boost::contract::old_ptr_if_copyable). For example, the following statements are equivalent:

auto old_x = BOOST_CONTRACT_OLDOF(x); // C++11 auto declarations always use `old_ptr` (never `old_ptr_if_copyable`).
boost::contract::old_ptr<decltype(x)> old_x = BOOST_CONTRACT_OLDOF(x);

If programmers want to relax the copyable type requirement, they must do so explicitly by using the boost::contract::old_ptr_if_copyable type instead of using auto declarations.

Old Value Type Traits
This library uses boost::contract::is_old_value_copyable to determine if an old value type is copyable or not, and then boost::contract::old_value_copy to actually copy the old value.
By default, boost::contract::is_old_value_copyable<T> is equivalent to boost::is_copy_constructible<T> and boost::contract::old_value_copy<T> is implemented using T's copy constructor. However, these type traits can be specialized by programmers for example to avoid making old value copies of types even when they have a copy constructor (maybe because these copy constructors are too expensive), or to make old value copies for types that do not have a copy constructor, or for any other specific need programmers might have for the types in question.
For example, the following specialization of boost::contract::is_old_value_copyable intentionally avoids making old value copies for all expressions of type w even if that type has a copy constructor (see old_if_copyable.cpp):

// Copyable type but...
class w {
public:
    w(w const&) { /* Some very expensive copy operation here... */ }

    /* ... */

// ...never copy old values for type `w` (because its copy is too expensive).
namespace boost { namespace contract {
    template<>
    struct is_old_value_copyable<w> : boost::false_type {};
} }

On the flip side, the following specializations of boost::contract::is_old_value_copyable and boost::contract::old_value_copy make old value copies of expressions of type p even if that type does not actually have a copy constructor (see old_if_copyable.cpp):

// Non-copyable type but...
class p : private boost::noncopyable {
    int* num_;

    friend struct boost::contract::old_value_copy<p>;

    /* ... */

// ...still copy old values for type `p` (using a deep copy).
namespace boost { namespace contract {
    template<>
    struct old_value_copy<p> {
        explicit old_value_copy(p const& old) {
            *old_.num_ = *old.num_; // Deep copy pointed value.
        }

        p const& old() const { return old_; }

    private:
        p old_;
    };

    template<>
    struct is_old_value_copyable<p> : boost::true_type {};
} }

In general, boost::is_copy_constructible and therefore boost::contract::is_old_value_copyable require C++11 decltype and SFINAE to automatically detect if a given type is copyable or not. On non-C++11 compilers, it is possible to inherit the old value type from boost::noncopyable, or use BOOST_MOVABLE_BUT_NOT_COPYABLE, or specialize boost::is_copy_constructible (see boost::is_copy_constructible documentation for more information), or just specialize boost::contract::is_old_value_copyable. For example, for a non-copyable type n the following code will work also on non-C++11 compilers (see old_if_copyable.cpp):

class n { // Do not want to use boost::noncopyable but...
    int num_;

private:
    n(n const&); // ...unimplemented private copy constructor (so non-copyable).

    /* ... */

// Specialize `boost::is_copy_constructible` (no need for this on C++11).
namespace boost { namespace contract {
    template<>
    struct is_old_value_copyable<n> : boost::false_type {};
} }

Assertion Requirements (Templates)
In general, assertions can introduce a new set of requirements on the types used by the program. Some of these type requirements might be necessary only to check the assertions and they would not be required by the program otherwise.
In some cases it might be acceptable, or even desirable, to cause a compile-time error when a program uses types that do not provide all the operations needed to check contract assertions (because it is not possible to fully check the correctness of the program as specified by its contracts). In these cases, programmers can specify contract assertions as we have seen so far, compilation will fail if user types do not provide all operations necessary to check the contracts.
However, in some other cases it might be desirable to not augment the type requirements of a program just because of contract assertions and to simply skip assertions when user types do not provide all the operations necessary to check them, without causing compile-time errors. Programmers can do this using if constexpr on C++17 compilers, and boost::contract::condition_if (or boost::contract::condition_if_c) on non-C++17 compilers.
For example, let's consider the following vector<T> class template equivalent to std::vector<T>. C++ std::vector<T> does not require that its value type parameter T has an equality operator == (it only requires T to be copy constructible, see std::vector documentation). However, the contracts for the vector<T>::push_back(value) public function include a postcondition back() == value that introduces the new requirement that T must also have an equality operator ==. Programmers can specify this postcondition as usual with BOOST_CONTRACT_ASSERT(back() == value) an let the program fail to compile when users instantiate vector<T> with a type T that does not provide an equality operator ==. Otherwise, programmers can guard this postcondition using C++17 if constexpr to evaluate the asserted condition only for types T that have an equality operator == and skip it otherwise. [74] For example:
[74] Rationale: [N1962] and other proposals to add contracts to C++ do not provide a mechanism to selectively disable assertions based on their type requirements. However, this library provides such a mechanism to allow to program contracts for template code without necessarily adding extra type requirements that would not be present if it was not for the contracts (so compiling the code with and without contracts will not alter the type requirements of the program). Something similar could be achieved combing C++17 if constexpr with [N1962] or [P0380] so that contract assertions within template code could be guarded by if constexpr statements checking the related type requirements ([N1962] already allows of if statements in contracts under the name of select assertions, [P0380] does not so probably if statements should be added to [P0380] as well). For example, assuming C++17 if constexpr can be used within [P0380] contracts:

template<typename T>
class vector {
public:
    void push_back(T const& value)
        [[ensures: if constexpr(boost::has_equal_to<T>::value) back() == value]]
    ...
};

template<typename T>
class vector {
public:
    void push_back(T const& value) {
        boost::contract::check c = boot::contract::public_function(this)
            .postcondition([&] {
                // Guard with `if constexpr` for T without `==`.
                if constexpr(boost::has_equal_to<T>::value)
                    BOOST_CONTRACT_ASSERT(back() == value);
            })
        ;

        vect_.push_back(value);
    }

    /* ... */

More in general, if constexpr can be used to guard a mix of both old value copies and contract assertions that introduce specific extra type requirements. For example, the following swap function can be called on any type T that is movable but its old value copies and postcondition assertions are evaluated only for types T that are also copyable and have an equality operator == (see if_constexpr.cpp):

template<typename T>
void swap(T& x, T& y) {
    constexpr bool b = boost::contract::is_old_value_copyable<T>::value &&
            boost::has_equal_to<T>::value;
    boost::contract::old_ptr<T> old_x, old_y;
    if constexpr(b) { // Contract requires copyable T...
        old_x = BOOST_CONTRACT_OLDOF(x);
        old_y = BOOST_CONTRACT_OLDOF(y);
    }
    boost::contract::check c = boost::contract::function()
        .postcondition([&] {
            if constexpr(b) { // ... and T with `==`...
                BOOST_CONTRACT_ASSERT(x == *old_y);
                BOOST_CONTRACT_ASSERT(y == *old_x);
            }
        })
    ;

    T t = std::move(x); // ...but body only requires movable T.
    x = std::move(y);
    y = std::move(t);
}

No if constexpr (no C++17)
On non-C++17 compilers where if constexpr is not available, it is possible to use boost::contract::condition_if to skip assertions based on type requirements (even if this code is less readable and more verbose than using if constexpr). For example (see condition_if.cpp):

template<typename T>
class vector {
public:
    void push_back(T const& value) {
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // Instead of `ASSERT(back() == value)` for T without `==`.
                BOOST_CONTRACT_ASSERT(
                    boost::contract::condition_if<boost::has_equal_to<T> >(
                        boost::bind(std::equal_to<T>(),
                            boost::cref(back()),
                            boost::cref(value)
                        )
                    )
                );
            })
        ;

        vect_.push_back(value);
    }

    /* ... */

More in general, boost::contract::condition_if is used as follow:

boost::contract::condition_if<Pred>(
    cond
)

Where Pred is a nullary boolean meta-function and cond is a nullary boolean functor. If Pred::value is statically evaluated to be true at compile-time then cond() is called at run-time and its boolean result is returned by the enclosing boost::contract::condition_if call. Otherwise, if Pred::value is statically evaluated to be false at compile-time then boost::contract::condition_if trivially returns true. Therefore, if cond is a functor template instantiation (not just a functor) then its call that contains the assertion operations with the extra type requirements (e.g., the equality operator ==) will not be actually instantiated and compiled unless the compiler determines at compile-time that Pred::value is true (when used this way, functor templates like std::equal_to and C++14 generic lambdas can be used to program cond, but C++11 lambdas cannot).
The boost::contract::condition_if function template is a special case of the more general boost::contract::call_if, specifically boost::contract::condition_if<Pred>(cond) is logically equivalent to boost::contract::call_if<Pred>(cond).else_([] { return true; }). [75] The boost::contract::call_if function template also accepts a number of optional else-if statements and one optional else statement:
[75] The internal implementation of boost::contract::condition_if is optimized and it does not actually use boost::contract::call_if.

boost::contract::call_if<Pred1>(
    t1
).template else_if<Pred2>(          // Optional.
    t2
)
...                                 // Optionally, other `else_if` statements.
.else_(                             // Optional for `void` functors, otherwise required.
    e
)

Where Pred1, Pred2, ... are nullary boolean meta-functions and t1, t2, ..., e are nullary functors. The return types of the functor calls t1(), t2(), ..., e() must either be all the same (including possibly all void) or be of types implicitly convertible into one another. At run-time boost::contract::call_if will call the functor t1(), or t2(), ..., or e() depending on which meta-function Pred1::value, Pred2::value, ... is statically evaluated to be true or false at compile-time, and it will return the value returned by the functor being called. If t1, t2, ..., e are functor template instantiations (not just functors) then their code will only be compiled if the compiler determines they need to be actually called at run-time (so only if the related Pred1::value, Pred2::value, ... are respectively evaluated to be true or false at compile-time). All the else_if<...>(...) statements are optional. The else_(...) statement is optional if the functor calls return void, otherwise it is required.
In general, boost::contract::call_if can be used to program contract assertions that compile and check different functor templates depending on related predicates being statically evaluated to be true or false at compile-time (but in most cases boost::contract::condition_if should be sufficient and less verbose to use). The boost::contract::condition_if_c, boost::contract::call_if_c, and .else_if_c function templates work similarly to their counterparts without the ..._c postfix seen so far, but they take their predicate template parameters as static boolean values instead of nullary boolean meta-functions.
On compilers that support C++17 if constexpr there should be no need to use boost::contract::condition_if or boost::contract::call_if because if constexpr can be used instead (making the code more readable and easier to program). [76]
[76] A part from its use within contracts, boost::contract::call_if can be used together with C++14 generic lambdas to emulate C++17 if constexpr (boost::hana::if_ and probably other approaches can also be used together with generic lambdas to emulate C++17 if constexpr on C++14 compilers). For example, the following implementation of myadvance will compile since C++14 and it is more concise, easier to read and maintain than the usual implementation of std::advance that uses tag dispatching (see call_if_cxx14.cpp):

template<typename Iter, typename Dist>
void myadvance(Iter& i, Dist n) {
    Iter* p = &i; // So captures change actual pointed iterator value.
    boost::contract::call_if<is_random_access_iterator<Iter> >(
        std::bind([] (auto p, auto n) { // C++14 generic lambda.
            *p += n;
        }, p, n)
    ).template else_if<is_bidirectional_iterator<Iter> >(
        std::bind([] (auto p, auto n) {
            if(n >= 0) while(n--) ++*p;
            else while(n++) --*p;
        }, p, n)
    ).template else_if<is_input_iterator<Iter> >(
        std::bind([] (auto p, auto n) {
            while(n--) ++*p;
        }, p, n)
    ).else_(
        std::bind([] (auto false_) {
            static_assert(false_, "requires at least input iterator");
        }, std::false_type()) // Use constexpr value.
    );
}

Of course, since C++17 the implementation that uses if constexpr is even more readable and concise:

template<typename Iter, typename Dist>
void myadvance(Iter& i, Dist n) {
    if constexpr(is_random_access_iterator<Iter>::value) {
        i += n;
    } else if constexpr(is_bidirectional_iterator<Iter>::value) {
        if(n >= 0) while(n--) ++i;
        else while(n++) --i;
    } else if constexpr(is_input_iterator<Iter>::value) {
        while(n--) ++i;
    } else {
        static_assert(false, "requires at least input iterator");
    }
}

Volatile Public Functions
This library allows to specify a different set of class invariants to check for volatile public functions. These volatile class invariants are programmed in a public const volatile function, named invariant, taking no argument, and returning void (see BOOST_CONTRACT_INVARIANT_FUNC to name the invariant function differently from invariant and Access Specifiers to not have to declare it public). Classes that do no have invariants for their volatile public functions, simply do not declare the void invariant() const volatile function.
In general, const volatile invariants work the same as const invariants (see Class Invariants) with the only difference that volatile and const volatile functions check const volatile invariants while non-const (i.e., neither const nor volatile) and const functions check const invariants. A given class can specify any combination of static, const volatile, and const invariant functions (see Class Invariants): [77]
[77] Rationale: Constructors and destructors check const volatile and const invariants in that order because the qualifier that can be applied to more calls is checked first (note that const volatile calls can be made on any object while const calls cannot be made on volatile objects, in that sense the const volatile qualifier can be applied to more calls than const alone can). This is consistent with static class invariants that are checked even before const volatile invariants (the static classifier can be applied to even more calls than const volatile, in fact an object is not even needed to make static calls).
Constructors check static invariants at entry and exit (even if an exception is thrown), plus const volatile and const invariants in that order at exit but only if no exception is thrown.
Destructors check static invariants at entry and exit (even if an exception is thrown), plus const volatile and const invariants in that order at entry (and at exit but only if an exception is thrown, even is destructors should in general never throw in C++).
Both non-const and const public functions check static and const invariants at entry and at exit (even if an exception is thrown).
Both volatile and const volatile public functions check static and const volatile invariants at entry and at exit (even if an exception is thrown).
These rules ensure that volatile class invariants are correctly checked (see Constructor Calls, Destructor Calls, and Public Function Calls). For example (see volatile.cpp):

class u {
public:
    static void static_invariant();     // Static invariants.
    void invariant() const volatile;    // Volatile invariants.
    void invariant() const;             // Const invariants.

    u() { // Check static, volatile, and const invariants.
        boost::contract::check c= boost::contract::constructor(this);
    }

    ~u() { // Check static, volatile, and const invariants.
        boost::contract::check c = boost::contract::destructor(this);
    }

    void nc() { // Check static and const invariants.
        boost::contract::check c = boost::contract::public_function(this);
    }

    void c() const { // Check static and const invariants.
        boost::contract::check c = boost::contract::public_function(this);
    }

    void v() volatile { // Check static and volatile invariants.
        boost::contract::check c = boost::contract::public_function(this);
    }

    void cv() const volatile { // Check static and volatile invariants.
        boost::contract::check c = boost::contract::public_function(this);
    }

    static void s() { // Check static invariants only.
        boost::contract::check c = boost::contract::public_function<u>();
    }
};

This library does not automatically check const volatile invariants for non-volatile functions. However, if the contract specifications require it, programmers can explicitly call the const volatile invariant function from the const invariant function (preferably in that order to be consistent with the order const volatile and const invariants are checked for constructors and destructors). That way all public functions, volatile or not, will check const volatile invariants (while only const and non-const public functions will check only const invariants, correctly so because the volatile qualifier shall not be stripped away): [78]
[78] Rationale: Note that while all public functions can be made to check const volatile invariants, it is never possible to make volatile public functions check const non-volatile invariants. That is because both const and volatile can always be added but never stripped in C++ (a part from forcefully via const_cast) but const is always automatically added by this library in order to enforce contract constant-correctness (see Constant-Correctness). That said, it would be too stringent for this library to also automatically add volatile and require all functions to check const volatile (not just const) invariants because only volatile members can be accessed from const volatile invariants so there could be many const (but not const volatile) members that are accessible from const invariants but not from const volatile invariants. To avoid this confusion, this library has chosen to draw a clear dichotomy between const and const volatile invariants so that only volatile public functions check const volatile invariants and only non-volatile public functions check const (but not const volatile) invariants. This is a clear distinction and it should serve most cases. If programmers need non-volatile public functions to also check const volatile invariants, they can explicitly do so by calling the const volatile invariant function from the const invariant function as shown in this documentation.

class u {
public:
    void invariant() const volatile { ... }                 // Volatile invariants.

    void invariant() const {
        auto const volatile* cv = this; cv->invariant();    // Call `const volatile` invariant function above.
        ...                                                 // Other non-volatile invariants.
    }

    ...
};

(As usual, private and protected functions do not check any invariant, not even when they are volatile or const volatile, see Private and Protected Functions).

Move Operations
As with all public operations of a class, also public move operations should maintain class invariants (see [Stroustrup13], p. 520). Specifically, at a minimum C++ requires the following:
The moved-from object can be copy assigned.
The moved-from object can be move assigned.
The moved-from object can be destroyed (if not for any other reason, this requires that class invariants are maintained by move operations because the destructor of the moved-from object requires class invariants to be satisfied at its entry, as always with destructors see Destructor Calls).
Therefore, both the move constructor and the move assignment operator need to maintain the class invariants of the moved-from object so their contracts can be programmed using boost::contract::constructor and boost::contract::public_function as usual. For example (see move.cpp):

class circular_buffer :
        private boost::contract::constructor_precondition<circular_buffer> {
public:
    void invariant() const {
        if(!moved()) { // Do not check (some) invariants for moved-from objects.
            BOOST_CONTRACT_ASSERT(index() < size());
        }
        // More invariants here that hold also for moved-from objects (e.g.,
        // all assertions necessary to successfully destroy moved-from objects).
    }

    // Move constructor.
    circular_buffer(circular_buffer&& other) :
        boost::contract::constructor_precondition<circular_buffer>([&] {
            BOOST_CONTRACT_ASSERT(!other.moved());
        })
    {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(!moved());
                BOOST_CONTRACT_ASSERT(other.moved());
            })
        ;

        move(std::forward<circular_buffer>(other));
    }

    // Move assignment.
    circular_buffer& operator=(circular_buffer&& other) {
        // Moved-from can be (move) assigned (so no pre `!moved()` here).
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(!other.moved());
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(!moved());
                BOOST_CONTRACT_ASSERT(other.moved());
            })
        ;

        return move(std::forward<circular_buffer>(other));
    }

    ~circular_buffer() {
        // Moved-from can always be destroyed (in fact no preconditions).
        boost::contract::check c = boost::contract::destructor(this);
    }

    bool moved() const {
        boost::contract::check c = boost::contract::public_function(this);
        return moved_;
    }

private:
    bool moved_;

    /* ... */

This example assumes that it is possible to call the public function moved() on the moved-from object. [79]
[79] In this example, the moved() function is simple enough that programmers could decide to not even call boost::contract::public_function from it for optimization reasons. However, calling boost::contract::public_function from moved() has no negative impact, a part from run-time overhead, because this library automatically disables contract checking while checking other contracts (so this call will not cause infinite recursion).
The default move constructor and move assignment operator generated by C++ will not automatically check contracts. Therefore, unless the move operations are not public or they have no preconditions, no postconditions, and their class has no invariants, programmers should manually define them using boost::contract::constructor, boost::contract::constructor_precondition, and boost::contract::public_function instead of relying on their default implementations generated by C++. (Same as for all other operations automatically implemented by C++.)
As always, programmers can decide to not program contracts for a given type. Specifically, they might decide to not program contracts for a class that needs to be moved in order to avoid the run-time overhead of checking contract assertions and to maximize performance (see Benefits and Costs).

Unions
A C++ union cannot have virtual functions, base classes, and cannot be used as a base class thus subcontracting (boost::contract::virtual_, BOOST_CONTRACT_OVERRIDE, etc.) do not apply to unions. Also a union cannot inherit from boost::contract::constructor_precondition (because it cannot have base classes), instead boost::contract::constructor_precondition is used to declare a local object that checks constructor preconditions (at the very beginning of the constructor before old value copies and other contracts, see declaration of pre in the example below). A part from that, this library is used as usual to program contracts for unions. For example (see union.cpp):

union positive {
public:
    static void static_invariant() { // Static class invariants (as usual).
        BOOST_CONTRACT_ASSERT(instances() >= 0);
    }

    void invariant() const { // Class invariants (as usual).
        BOOST_CONTRACT_ASSERT(i_ > 0);
        BOOST_CONTRACT_ASSERT(d_ > 0);
    }

    // Contracts for constructor, as usual but...
    explicit positive(int x) : d_(0) {
        // ...unions cannot have bases so constructor preconditions here.
        boost::contract::constructor_precondition<positive> pre([&] {
            BOOST_CONTRACT_ASSERT(x > 0);
        });
        boost::contract::old_ptr<int> old_instances =
                BOOST_CONTRACT_OLDOF(instances());
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                { int y; get(y); BOOST_CONTRACT_ASSERT(y == x); }
                BOOST_CONTRACT_ASSERT(instances() == *old_instances + 1);
            })
        ;

        i_ = x;
        ++instances_;
    }

    // Contracts for destructor (as usual).
    ~positive() {
        boost::contract::old_ptr<int> old_instances =
                BOOST_CONTRACT_OLDOF(instances());
        boost::contract::check c = boost::contract::destructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(instances() == *old_instances - 1);
            })
        ;

        --instances_;
    }

    // Contracts for public function (as usual, but no virtual or override).
    void get(int& x) const {
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(x > 0);
            })
        ;

        x = i_;
    }

    // Contracts for static public function (as usual).
    static int instances() {
        boost::contract::check c = boost::contract::public_function<positive>();
        return instances_;
    }

private:
    int i_;
    double d_;

    /* ... */

Assertion Levels
This library provides three predefined assertion levels that can be used to selectively disable assertions depending on their computational complexity: [80]
[80] The assertion levels predefined by this library are similar to the default, audit, and axiom levels from [P0380].
BOOST_CONTRACT_ASSERT is used to assert conditions that are not computationally expensive, at least compared to the cost of executing the function body. These assertions are the ones we have seen so far, they are always checked at run-time and they cannot be disabled.
BOOST_CONTRACT_ASSERT_AUDIT is used to assert conditions that are computationally expensive compared to the cost of executing the function body. These assertions are not checked at run-time unless programmers explicitly define BOOST_CONTRACT_AUDITS (undefined by default), but the asserted conditions are always compiled and therefore validated syntactically (even when they are not actually evaluated and checked at run-time).
BOOST_CONTRACT_ASSERT_AXIOM is used to assert conditions that are computationally prohibitive, at least compared to the cost of executing the function body. These assertions are never evaluated or checked at run-time, but the asserted conditions are always compiled and therefore validated syntactically (so these assertions can serve as formal comments to the code).
In addition, BOOST_CONTRACT_CHECK_AUDIT and BOOST_CONTRACT_CHECK_AXIOM are similar to BOOST_CONTRACT_ASSERT_AUDIT and BOOST_CONTRACT_ASSERT_AXIOM but they are used to program audit and axiom levels for implementation checks instead of assertions (see Implementation Checks).
For example, BOOST_CONTRACT_ASSERT_AUDIT can be used to program computationally expensive assertions (see assertion_level.cpp):

template<typename RandomIter, typename T>
RandomIter random_binary_search(RandomIter first, RandomIter last,
        T const& value) {
    RandomIter result;
    boost::contract::check c = boost::contract::function()
        .precondition([&] {
            BOOST_CONTRACT_ASSERT(first <= last); // Default, not expensive.
            // Expensive O(n) assertion (use AXIOM if prohibitive instead).
            BOOST_CONTRACT_ASSERT_AUDIT(std::is_sorted(first, last));
        })
        .postcondition([&] {
            if(result != last) BOOST_CONTRACT_ASSERT(*result == value);
        })
    ;

    /* ... */

Similarly, BOOST_CONTRACT_AUDITS can be used to disable expensive old value copies and related assertions that use them (see assertion_level.cpp):

template<typename T>
class vector {

public:
    void swap(vector& other) {
        boost::contract::old_ptr<vector> old_me, old_other;
        #ifdef BOOST_CONTRACT_AUDITS
            old_me = BOOST_CONTRACT_OLDOF(*this);
            old_other = BOOST_CONTRACT_OLDOF(other);
        #endif // Else, skip old value copies...
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // ...and also skip related assertions.
                BOOST_CONTRACT_ASSERT_AUDIT(*this == *old_other);
                BOOST_CONTRACT_ASSERT_AUDIT(other == *old_me);
            })
        ;

        vect_.swap(other.vect_);
    }

    /* ... */

private:
    std::vector<T> vect_;
};

The condition passed to BOOST_CONTRACT_ASSERT_AXIOM is compiled but not actually evaluated at run-time so this macro can be used to program computationally prohibitive assertions but also assertions that cannot actually be programmed in C++ using functions that are declared but left undefined. For example, (see assertion_level.cpp):

// If valid iterator range (cannot implement in C++ but OK to use in AXIOM).
template<typename Iter>
bool valid(Iter first, Iter last); // Only declared, not actually defined.

template<typename T>
class vector {

public:
    iterator insert(iterator where, T const& value) {
        iterator result;
        boost::contract::old_ptr<unsigned> old_capacity =
                BOOST_CONTRACT_OLDOF(capacity());
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
                if(capacity() > *old_capacity) {
                    BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end()));
                } else {
                    BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end()));
                }
            })
        ;

        return result = vect_.insert(where, value);
    }

    /* ... */

private:
    std::vector<T> vect_;
};

In addition to these assertion levels that are predefined by this library, programmers are free to define their own. For example, the following macro could be used to program and selectively disable assertions that have exponential computational complexity O(e^n):

#ifdef EXPONENTIALLY_COMPLEX_ASSERTIONS
    // Following will compile and also evaluate `cond`.
    #define ASSERT_EXP(cond) BOOST_CONTRACT_ASSERT(cond)
#else
    // Following will compile but never actually evaluate `cond`.
    #define ASSERT_EXP(cond) BOOST_CONTRACT_ASSERT(true || (cond))
#endif

...

ASSERT_EXP(some-exponentially-complex-boolean-condition);

Disable Contract Checking
Checking contracts adds run-time overhead and can slow down program execution (see Benefits and Costs). Therefore, programmers can define any combination of the following macros (-D option in Clang and GCC, /D option in MSVC, etc.) to instruct this library to not check specific groups of contract conditions at run-time:
Define BOOST_CONTRACT_NO_PRECONDITIONS to not check preconditions.
Define BOOST_CONTRACT_NO_POSTCONDITIONS to not check postconditions.
Define BOOST_CONTRACT_NO_EXCEPTS to not check exception guarantees.
Define BOOST_CONTRACT_NO_ENTRY_INVARIANTS to not check class invariants at call entry.
Define BOOST_CONTRACT_NO_EXIT_INVARIANTS to not check class invariants at call exit.
Or, define BOOST_CONTRACT_NO_INVARIANTS to not check class invariants at both call entry and exit. (This is provided for convenience, it is equivalent to defining both BOOST_CONTRACT_NO_ENTRY_INVARIANTS and BOOST_CONTRACT_NO_EXIT_INVARIANTS.)
Define BOOST_CONTRACT_NO_CHECKS to not evaluate implementation checks.
Old values can be used by both postconditions and exception guarantees so it is necessary to define both BOOST_CONTRACT_NO_POSTCONDITIONS and BOOST_CONTRACT_NO_EXCEPTS to disable old value copies.
By default, none of these macros are defined so this library checks all contracts. When these macros are defined by the user, the implementation code of this library is internally optimized to minimize as much as possible any run-time and compile-time overhead associated with checking and compiling contracts (see Disable Contract Compilation for techniques to completely remove any run-time and compile-time overheads associated with contract code).
For example, programmers could decide to check all contracts during early development builds, but later check only preconditions and maybe entry invariants for release builds by defining BOOST_CONTRACT_NO_POSTCONDITIONS, BOOST_CONTRACT_NO_EXCEPTS, BOOST_CONTRACT_NO_EXIT_INVARIANTS, and BOOST_CONTRACT_NO_CHECKS.

Disable Contract Compilation (Macro Interface)
This library provides macros that can be used to completely disable compile-time and run-time overhead introduced by contracts but at the cost of manually programming #ifndef BOOST_CONTRACT_NO_... statements around contract code:
This library defines BOOST_CONTRACT_NO_CONSTRUCTORS when contract checking is disabled for constructors.
This library defines BOOST_CONTRACT_NO_DESTRUCTORS when contract checking is disabled for destructors.
This library defines BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS when contract checking is disabled for public functions.
This library defines BOOST_CONTRACT_NO_FUNCTIONS when contract checking is disabled for (non-public and non-member) functions.
This library defines BOOST_CONTRACT_NO_OLDS when old value copies are disabled.
This library defines BOOST_CONTRACT_NO_ALL when all contracts above and also implementation checks (see BOOST_CONTRACT_NO_CHECKS) are disabled.
These macros are not configuration macros and they should not be defined directly by programmers (otherwise this library will generate compile-time errors). Instead, these macros are automatically defined by this library when programmers define BOOST_CONTRACT_NO_PRECONDITIONS, BOOST_CONTRACT_NO_POSTCONDITIONS, BOOST_CONTRACT_NO_EXCEPTS, BOOST_CONTRACT_NO_INVARIANTS (or BOOST_CONTRACT_NO_ENTRY_INVARIANTS and BOOST_CONTRACT_NO_EXIT_INVARIANTS), and BOOST_CONTRACT_NO_CHECKS (see Disable Contract Checking).
Alternatively, this library provides a macro-based interface defined in boost/contract_macro.hpp that can also be used to completely disable compile-time and run-time overheads introduced by contracts but without the burden of manually writing the #ifndef BOOST_CONTRACT_NO_... statements. For example, the following code shows how to use both the boost/contract_macro.hpp macro interface and the #ifndef BOOST_CONTRACT_NO_... statements to completely disable compile-time and run-time overheads for non-member function contracts (see ifdef_macro.cpp and ifdef.cpp):
Macro Interface	#ifndef BOOST_CONTRACT_NO_... Statements
// Use macro interface to completely disable contract code compilation. #include <boost/contract_macro.hpp> int inc(int& x) { int result; BOOST_CONTRACT_OLD_PTR(int)(old_x, x); BOOST_CONTRACT_FUNCTION() BOOST_CONTRACT_PRECONDITION([&] { BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); }) BOOST_CONTRACT_POSTCONDITION([&] { BOOST_CONTRACT_ASSERT(x == *old_x + 1); BOOST_CONTRACT_ASSERT(result == *old_x); }) ; return result = x++; }	// Use #ifdef to completely disable contract code compilation. #include <boost/contract/core/config.hpp> #ifndef BOOST_CONTRACT_NO_ALL #include <boost/contract.hpp> #endif int inc(int& x) { int result; #ifndef BOOST_CONTRACT_NO_OLDS boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); #endif #ifndef BOOST_CONTRACT_NO_FUNCTIONS boost::contract::check c = boost::contract::function() #ifndef BOOST_CONTRACT_NO_PRECONDITIONS .precondition([&] { BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); }) #endif #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS .postcondition([&] { BOOST_CONTRACT_ASSERT(x == *old_x + 1); BOOST_CONTRACT_ASSERT(result == *old_x); }) #endif ; #endif return result = x++; }
The same can be done to disable contract code complication for private and protected functions. The BOOST_CONTRACT_OLD_PTR_IF_COPYABLE macro is provided to handle non-copyable old value types (similar to boost::contract::old_ptr_if_copyable).
For constructors, destructors, and public functions the boost/contract_macro.hpp macro interface and the #ifndef BOOST_CONTRACT_NO_... statements can be used as follow (see ifdef_macro.cpp and ifdef.cpp):
Macro Interface	#ifndef BOOST_CONTRACT_NO_... Statements
class integers #define BASES public pushable<int> : // Left in code (almost no overhead). private boost::contract::constructor_precondition<integers>, BASES { // Followings left in code (almost no overhead). friend class boost::contract::access; typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; #undef BASES BOOST_CONTRACT_INVARIANT({ BOOST_CONTRACT_ASSERT(size() <= capacity()); }) public: integers(int from, int to) : BOOST_CONTRACT_CONSTRUCTOR_PRECONDITION(integers)([&] { BOOST_CONTRACT_ASSERT(from <= to); }), vect_(to - from + 1) { BOOST_CONTRACT_CONSTRUCTOR(this) BOOST_CONTRACT_POSTCONDITION([&] { BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1)); }) ; for(int x = from; x <= to; ++x) vect_.at(x - from) = x; } virtual ~integers() { BOOST_CONTRACT_DESTRUCTOR(this); // Check invariants. } virtual void push_back( int const& x, boost::contract::virtual_* v = 0 // Left in code (almost no overhead). ) /* override */ { BOOST_CONTRACT_OLD_PTR(unsigned)(old_size); BOOST_CONTRACT_PUBLIC_FUNCTION_OVERRIDE(override_push_back)( v, &integers::push_back, this, x) BOOST_CONTRACT_PRECONDITION([&] { BOOST_CONTRACT_ASSERT(size() < max_size()); }) BOOST_CONTRACT_OLD([&] { old_size = BOOST_CONTRACT_OLDOF(v, size()); }) BOOST_CONTRACT_POSTCONDITION([&] { BOOST_CONTRACT_ASSERT(size() == *old_size + 1); }) BOOST_CONTRACT_EXCEPT([&] { BOOST_CONTRACT_ASSERT(size() == *old_size); }) ; vect_.push_back(x); } private: BOOST_CONTRACT_OVERRIDE(push_back) // Left in code (almost no overhead). /* ... */	class integers #define BASES public pushable<int> : #ifndef BOOST_CONTRACT_NO_PRECONDITIONS private boost::contract::constructor_precondition<integers>, BASES #else BASES #endif { #ifndef BOOST_CONTRACT_NO_ALL friend class boost::contract::access; #endif #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; #endif #undef BASES #ifndef BOOST_CONTRACT_NO_INVARIANTS void invariant() const { BOOST_CONTRACT_ASSERT(size() <= capacity()); } #endif public: integers(int from, int to) : #ifndef BOOST_CONTRACT_NO_PRECONDITIONS boost::contract::constructor_precondition<integers>([&] { BOOST_CONTRACT_ASSERT(from <= to); }), #endif vect_(to - from + 1) { #ifndef BOOST_CONTRACT_NO_CONSTRUCTORS boost::contract::check c = boost::contract::constructor(this) #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS .postcondition([&] { BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1)); }) #endif ; #endif for(int x = from; x <= to; ++x) vect_.at(x - from) = x; } virtual ~integers() { #ifndef BOOST_CONTRACT_NO_DESTRUCTORS // Check invariants. boost::contract::check c = boost::contract::destructor(this); #endif } virtual void push_back( int const& x #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS , boost::contract::virtual_* v = 0 #endif ) /* override */ { #ifndef BOOST_CONTRACT_NO_OLDS boost::contract::old_ptr<unsigned> old_size; #endif #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS boost::contract::check c = boost::contract::public_function< override_push_back>(v, &integers::push_back, this, x) #ifndef BOOST_CONTRACT_NO_PRECONDITIONS .precondition([&] { BOOST_CONTRACT_ASSERT(size() < max_size()); }) #endif #ifndef BOOST_CONTRACT_NO_OLDS .old([&] { old_size = BOOST_CONTRACT_OLDOF(v, size()); }) #endif #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == *old_size + 1); }) #endif #ifndef BOOST_CONTRACT_NO_EXCEPTS .except([&] { BOOST_CONTRACT_ASSERT(size() == *old_size); }) #endif ; #endif vect_.push_back(x); } private: #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS BOOST_CONTRACT_OVERRIDE(push_back) #endif /* ... */
Static and volatile class invariants can be programmed using BOOST_CONTRACT_STATIC_INVARIANT and BOOST_CONTRACT_INVARIANT_VOLATILE respectively (these macros expand code equivalent to the static void BOOST_CONTRACT_STATIC_INVARIANT_FUNC() and void BOOST_CONTRACT_INVARIANT_FUNC() const volatile functions).
The boost/contract_macro.hpp macro interface is usually preferred because more concise and easier to use than programming #ifndef BOOST_CONTRACT_NO_... statements by hand. However, C++ macros expand on a single line of code and that can make compiler errors less useful when using this macro interface plus all contract assertions within a given set of preconditions, postconditions, exception guarantees, and class invariants will list the same line number in error messages when assertions fail at run-time (but error messages still list the assertion code and that should still allow programmers to identify the specific assertion that failed). Finally, the macro interface leaves a bit of contract decorations in the code but that should add no measurable compile-time or run-time overhead (specifically, extra boost::contract::virtual_* parameters, calls to boost::contract::constructor_precondition default constructor which does nothing, BOOST_CONTRACT_BASE_TYPES typedefs, and boost::contract::access friendships are left in user code even when contracts are disabled unless #ifndef BOOST_CONTRACT_NO_... statements are used).
Disabling contract as shown in Disable Contract Checking leaves the overhead of compiling contract code plus some small run-time overhead due to the initialization of old value pointers (even if those will be all null and no old value will be actually copied), the calls to the contract functions used to initialize boost::contract::check and boost::contract::constructor_precondition (even if those calls will be internally optimized by this library to essentially do nothing), etc. For truly performance critical code for which even such small run-time overhead might not be acceptable, the macro interface (or the #ifndef BOOST_CONTRACT_NO_... statements) can be used to completely disable compile-time and run-time overheads of contracts. However, for such performance critical code even the overhead of checking simple preconditions might be too much so it might be best to not program contracts at all.
Usually, if the overhead of checking preconditions and other assertions is already considered acceptable for an application then the compile-time overhead of contracts should not represent an issue and it should be sufficient to disable contract checking at run-time as indicated in Disable Contract Checking (without a real need to use the boost/contract_macro.hpp macro interface or the #ifndef BOOST_CONTRACT_NO_... statements in most cases).

Separate Body Implementation
Contracts are part of the program specifications and not of its implementation (see Specifications vs. Implementation). However, this library uses function definitions to program contracts so contract code appears together with the function implementation code. This is not ideal (even if contracts programmed using this library will always appear at the very beginning of the function definition so programmers will easily be able to distinguish contract code from the rest of the function implementation code so this might not be real limitation in practise).
In some cases, it might be desirable to completely separate the contract code from the function implementation code. For example, this could be necessary for software that ships only header files and compiled object files to its users. If contracts are programmed in function definitions that are compiled in the object files, users will not be able to see the contract code to understand semantics and usage of the functions (again, this might not be a real problem in practice for example if contracts are already somehow extracted from the source code by some tool and presented as part of the documentation of the shipped software).
In any case, when it is truly important to separate contracts from function implementation code, function implementations can be programmed in extra body functions (here named ..._body, but any other naming scheme could be used) that are compiled in object files. Function definitions that remain in header files instead will contain just contract code followed by calls to the extra body functions. This technique allows to keep the contract code in header files while separating the implementation code to source and object files. However, this adds the overhead of manually programming an extra function declaration for each body function (plus the limitation that constructor member initialization lists must be programmed in header files because that is where constructors need to be defined to list constructor contract code). [81]
[81] When used as default parameter values, lambda functions allow to program code statements within function declarations. However, these lambadas cannot be effectively used to program contracts in function declarations instead of definitions. That is because the C++11 standard does not allow lambdas in function declarations to capture any variable (for the good reason that it is not at all obvious how to correctly define the semantics of such captures). For example, the following code is not valid C++ and it does not compile:

// Specifications (in declaration).
int inc(int& x,
    // Error: Lambdas in default parameters cannot capture `this`, `x`, or any other variable.
    std::function<void ()> pre = [&] {
        BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max());
    },
    std::function<void (int const&, boost::contract::old_ptr<int> const&)> post
        = [&] (int const& result, boost::contract::old_ptr<int> const& old_x)
    {
        BOOST_CONTRACT_ASSERT(x == *old_x + 1);
        BOOST_CONTRACT_ASSERT(result == *old_x);
    }
);

// Implementation (in definition).
int inc(int& x,
    std::function<void ()> pre,
    std::function<void (int const&, boost::contract::old_ptr<int> const&)> post
) {
    int result;
    boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x);
    boost::contract::check c = boost::contract::function()
        .precondition(pre)
        .postcondition(std::bind(post, std::cref(result), std::cref(old_x)))
    ;

    return result = x++; // Function body.
}

In any case, even if the above code compiled, it would require significant boiler-plate code to bind return and old values.
For example, the following header file only contains function declarations, contract code, and constructor member initializations, but it does not contain the code implementing the function bodies (see separate_body.hpp):

class iarray :
        private boost::contract::constructor_precondition<iarray> {
public:
    void invariant() const {
        BOOST_CONTRACT_ASSERT(size() <= capacity());
    }

    explicit iarray(unsigned max, unsigned count = 0) :
        boost::contract::constructor_precondition<iarray>([&] {
            BOOST_CONTRACT_ASSERT(count <= max);
        }),
        // Still, member initializations must be here.
        values_(new int[max]),
        capacity_(max)
    {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(capacity() == max);
                BOOST_CONTRACT_ASSERT(size() == count);
            })
        ;
        constructor_body(max, count); // Separate constructor body impl.
    }

    virtual ~iarray() {
        boost::contract::check c = boost::contract::destructor(this); // Inv.
        destructor_body(); // Separate destructor body implementation.
    }

    virtual void push_back(int value, boost::contract::virtual_* v = 0) {
        boost::contract::old_ptr<unsigned> old_size =
                BOOST_CONTRACT_OLDOF(v, size());
        boost::contract::check c = boost::contract::public_function(v, this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(size() < capacity());
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
            })
        ;
        push_back_body(value); // Separate member function body implementation.
    }

private:
    // Contracts in class declaration (above), but body implementations are not.
    void constructor_body(unsigned max, unsigned count);
    void destructor_body();
    void push_back_body(int value);

    /* ... */

Instead, the function bodies are implemented in a separate source file (see separate_body.cpp):

void iarray::constructor_body(unsigned max, unsigned count) {
    for(unsigned i = 0; i < count; ++i) values_[i] = int();
    size_ = count;
}

void iarray::destructor_body() { delete[] values_; }

void iarray::push_back_body(int value) { values_[size_++] = value; }

/* ... */

The same technique can be used for non-member, private, and protected functions, etc.
When contracts are programmed only in .cpp files and also all this library headers are #included only from .cpp files, then these .cpp files can be compiled disabling specific contract checking (for example, BOOST_CONTRACT_NO_POSTCONDITIONS, BOOST_CONTRACT_NO_EXCEPTS, and BOOST_CONTRACT_NO_EXIT_INVARIANTS, see Disable Contract Checking). Then the code in these .cpp files will always have such contract checking disabled even when linked to some other user code that might have been compiled with a different set of contracts disabled (i.e., a different set of BOOST_CONTRACT_NO_... macros defined). This technique might be useful to ship compiled object files (e.g., for a library) that will never check some contracts (e.g., postconditions, exception guarantees, and exit invariants) regardless of the definition of the BOOST_CONTRACT_NO_... macros used to compile code that links against the shipped object files.
On the flip side, if contracts are programmed only in header files (e.g., using extra ..._body functions as shown in this section) and this library headers are #included only in these header files that are being shipped, then end users can enable or disables contract checking of the shipped code by defining the BOOST_CONTRACT_NO_... macros when they compile the shipped header files as part of their code. This technique might be useful in other situations when programmers that ship code want to leave it up the their end users to decide which contracts of the shipped code should be checked at run-time.

No Lambda Functions (No C++11)
This section shows how to use this library without C++11 lambda functions. This has some advantages:
It allows to use this library on compilers that do not support C++11 lambda functions (essentially most C++03 compilers with adequate support for SFINAE can be used in that case, see No Macros to also avoid using variadic macros). [82]
[82] Alternatively, on compilers that do not support C++11 lambda functions, Boost.LocalFunction could be used to program the contract functors still within the function definitions (for example, see no_lambda_local_func.cpp). In general, such a code is less verbose than the example shown in this section that uses contract functions programmed outside of the original function definitions (about 30% less lines of code) but the contract code is hard to read. Other libraries could also be used to program the contract functors without C++11 lambda functions (Boost.Lambda, Boost.Fusion, etc.) but again all these techniques will result in contract code either more verbose, or harder to read and maintain than the code that uses C++11 lambda functions.
Contract functions (i.e., the ..._precondition, ..._old, and ..._postcondition functions in the example below) can be programmed to fully enforce constant-correctness and other contract requirements at compile-time (see Constant-Correctness). [83]
[83] If C++ allowed lambda functions to capture variables by constant reference (for example allowing a syntax like this [const&] { ... } and [const& variable-name] { ... }, see https://groups.google.com/a/isocpp.org/forum/#!topic/std-proposals/0UKQw9eo3N0) also lambdas could be used to program contract functors that fully enforce Constant-Correctness at compile-time. Note that C++11 lambdas allow to capture variables by value (using [=] { ... } and [variable-name] { ... }) and these value captures are const (unless the lambda is explicitly declared mutable) but they are not suitable to program postconditions and exception guarantees using this library (because those require capturing by reference, see Postconditions and Exception Guarantees), plus they introduce a copy of the captured value that might be too expensive in general and therefore not suitable for preconditions either.
Code of the contract functions is separated from function body implementations (see Separate Body Implementation).
However, not using C++11 lambda functions comes at the significant cost of having to manually program the extra contract functions and related boiler-plate code. For example, the header file (see no_lambdas.hpp):

class iarray :
        private boost::contract::constructor_precondition<iarray> {
public:
    static void static_invariant() {
        BOOST_CONTRACT_ASSERT(instances() >= 0);
    }

    void invariant() const {
        BOOST_CONTRACT_ASSERT(size() <= capacity());
    }

    explicit iarray(unsigned max, unsigned count = 0);
        static void constructor_precondition(unsigned const max,
                unsigned const count) {
            BOOST_CONTRACT_ASSERT(count <= max);
        }
        static void constructor_old(boost::contract::old_ptr<int>&
                old_instances) {
            old_instances = BOOST_CONTRACT_OLDOF(instances());
        }
        void constructor_postcondition(unsigned const max, unsigned const count,
                boost::contract::old_ptr<int> const old_instances) const {
            BOOST_CONTRACT_ASSERT(capacity() == max);
            BOOST_CONTRACT_ASSERT(size() == count);
            BOOST_CONTRACT_ASSERT(instances() == *old_instances + 1);
        }

    virtual ~iarray();
        void destructor_old(boost::contract::old_ptr<int>& old_instances)
                const {
            old_instances = BOOST_CONTRACT_OLDOF(instances());
        }
        static void destructor_postcondition(boost::contract::old_ptr<int> const
                old_instances) {
            BOOST_CONTRACT_ASSERT(instances() == *old_instances - 1);
        }

    virtual void push_back(int value, boost::contract::virtual_* v = 0);
        void push_back_precondition() const {
            BOOST_CONTRACT_ASSERT(size() < capacity());
        }
        void push_back_old(boost::contract::virtual_* v,
                boost::contract::old_ptr<unsigned>& old_size) const {
            old_size = BOOST_CONTRACT_OLDOF(v, size());
        }
        void push_back_postcondition(
                boost::contract::old_ptr<unsigned> const old_size) const {
            BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
        }

    unsigned capacity() const;
    unsigned size() const;

    static int instances();

private:
    int* values_;
    unsigned capacity_;
    unsigned size_;
    static int instances_;
};

And, the source file (see no_lambdas.cpp):

iarray::iarray(unsigned max, unsigned count) :
    boost::contract::constructor_precondition<iarray>(boost::bind(
            &iarray::constructor_precondition, max, count)),
    values_(new int[max]), // Member initializations can be here.
    capacity_(max)
{
    boost::contract::old_ptr<int> old_instances;
    boost::contract::check c = boost::contract::constructor(this)
        .old(boost::bind(&iarray::constructor_old, boost::ref(old_instances)))
        .postcondition(boost::bind(
            &iarray::constructor_postcondition,
            this,
            boost::cref(max),
            boost::cref(count),
            boost::cref(old_instances)
        ))
    ;

    for(unsigned i = 0; i < count; ++i) values_[i] = int();
    size_ = count;
    ++instances_;
}

iarray::~iarray() {
    boost::contract::old_ptr<int> old_instances;
    boost::contract::check c = boost::contract::destructor(this)
        .old(boost::bind(&iarray::destructor_old, this,
                boost::ref(old_instances)))
        .postcondition(boost::bind(&iarray::destructor_postcondition,
                boost::cref(old_instances)))
    ;

    delete[] values_;
    --instances_;
}

void iarray::push_back(int value, boost::contract::virtual_* v) {
    boost::contract::old_ptr<unsigned> old_size;
    boost::contract::check c = boost::contract::public_function(v, this)
        .precondition(boost::bind(&iarray::push_back_precondition, this))
        .old(boost::bind(&iarray::push_back_old, this, boost::cref(v),
                boost::ref(old_size)))
        .postcondition(boost::bind(&iarray::push_back_postcondition, this,
                boost::cref(old_size)))
    ;

    values_[size_++] = value;
}

unsigned iarray::capacity() const {
    // Check invariants.
    boost::contract::check c = boost::contract::public_function(this);
    return capacity_;
}

unsigned iarray::size() const {
    // Check invariants.
    boost::contract::check c = boost::contract::public_function(this);
    return size_;
}

int iarray::instances() {
    // Check static invariants.
    boost::contract::check c = boost::contract::public_function<iarray>();
    return instances_;
}

int iarray::instances_ = 0;

If programmers also want to fully enforce all contract programming constant-correctness requirements at compile-time, they should follow these rules when programming the contract functions (see Constant-Correctness):
Precondition functions (i.e., the ..._precondition functions in the example above) can take their arguments either by const value or by const&, and when they are member functions they should be either static or const functions.
Postcondition functions (i.e., the ..._postcondition functions in the example above) should take their arguments by const&, and when they are member functions they should be either static or const functions.
Similarly, exception guarantee functions (not shown in the example above) should take their arguments by const&, and when they are member functions they should be either static or const functions.
Old value functions (i.e., the ..._old functions in the example above) should take their arguments by const& a part from old value pointers that should be taken by & (so only old value pointers can be modified), and when they are member functions they should be either static or const functions.
For constructors: Precondition, old value, and exception guarantee functions should be static (because there is no valid object this if the constructor body does not run successfully, see Constructor Calls).
For destructors: Postcondition functions should be static (because there is no valid object this after the destructor body runs successfully, but exception guarantee functions do not have to be static since the object this is still valid because the destructor body did not run successfully, see Destructor Calls).
Note that the extra contract functions also allow to keep the contract code in the header file while all function bodies are implemented in a separate source file (including the constructor member initialization list, that could not be done with the techniques shown in Separate Body Implementation). [84] Also note that the contract functions can always be declared private if programmers need to exactly control the public members of the class (this was not done in this example only for brevity).
[84] In this example, bind was used to generate nullary functors from the contract functions. As always with bind, cref and ref must be used to bind arguments by const& and & respectively, plus it might be necessary to explicitly static_cast the function pointer passed to bind for overloaded functions.
The authors think this library is most useful when used together with C++11 lambda functions (because of the large amount of boiler-plate code required when C++11 lambdas are not used as also shown by the example above).

No Macros (and No Variadic Macros)
It is possible to specify contracts without using most of the macros provided by this library and programming the related code manually instead (the only macros that cannot be programmed manually are BOOST_CONTRACT_OVERRIDE, BOOST_CONTRACT_OVERRIDES, and BOOST_CONTRACT_NAMED_OVERRIDE).
Some of this library macros are variadic macros, others are not (see below). Variadic macros were officially added to the language in C++11 but most compilers have been supporting them as an extension for a long time, plus all compilers that support C++11 lambda functions should also support C++11 variadic macros (and this library might rarely be used without the convenience of C++11 lambda functions, see No Lambda Functions). [85] Therefore, the rest of this section can be considered mainly a curiosity because programmers should seldom, if ever, need to use this library without using its macros.
[85] Compilation times of this library were measured to be comparable between compilers that support variadic macros and compilers that do not.

Overrides
As shown in Public Function Overrides and Named Overrides, this library provides the BOOST_CONTRACT_OVERRIDE and BOOST_CONTRACT_NAMED_OVERRIDE macros to program contracts for overriding public functions (see BOOST_CONTRACT_MAX_ARGS for compilers that do not support variadic templates). [86] These macro cannot be programmed manually but they are not variadic macros (so programmers should be able to use them on any C++ compiler with a sound support for SFINAE). [87] The BOOST_CONTRACT_OVERRIDES macro is a variadic macro instead but programmes can manually repeat the non-variadic macro BOOST_CONTRACT_OVERRIDE for each overriding public function name on compilers that do not support variadic macros.
[86] Rationale: The BOOST_CONTRACT_MAX_ARGS macro is named after BOOST_FUNCTION_MAX_ARGS.
[87] Rationale: These macros expand to SFINAE-based introspection template code that are too complex to be programmed manually by users (that remains the case even if C++14 generic lambdas were to be used here). On a related note, in theory using C++14 generic lambdas, the BOOST_CONTRACT_OVERRIDE macro could be re-implemented in a way that can be expanded at function scope, instead of class scope (but there is not really a need to do that).

Assertions (Not Variadic)
As shown in Preconditions, Postconditions, Exception Guarantees, Class Invariants, etc. this library provides the BOOST_CONTRACT_ASSERT macro to assert contract conditions. This is not a variadic macro and programmers should be able to use it on all C++ compilers. In any case, the invocation BOOST_CONTRACT_ASSERT(cond) simply expands to code equivalent to the following: [88]
[88] Rationale: There is no need for the code expanded by BOOST_CONTRACT_ASSERT to also use C++11 __func__. That is because __func__ will always expand to the name operator() of the functor used to program the contract assertions (e.g., the internal name the compiler assigns to lambda functions) and it will not expand to the name of the actual function enclosing the contract declaration.

if(!(cond)) {
    throw boost::contract::assertion_failure(__FILE__, __LINE__,
            BOOST_PP_STRINGIZE(cond));
}

In fact, this library considers any exception thrown from within preconditions, postconditions, exception guarantees, and class invariants as a contract failure and reports it calling the related contract failure handler (boost::contract::precondition_failure, etc.). If there is a need for it, programmers can always program contract assertions that throw specific user-defined exceptions as follow (see Throw on Failures):

if(!cond) throw exception-object;

However, using BOOST_CONTRACT_ASSERT is convenient because it always allows this library to show an informative message in case of assertion failure containing the assertion code, file name, line number, etc.
As shown in Assertion Levels, this library pre-defines BOOST_CONTRACT_ASSERT_AUDIT and BOOST_CONTRACT_ASSERT_AXIOM assertion levels. These macros are not variadic macros and programmers should be able to use them on all C++ compilers. In any case, their implementations are equivalent to the following:

#ifdef BOOST_CONTRACT_AUDITS
    #define BOOST_CONTRACT_ASSERT_AUDIT(cond) \
        BOOST_CONTRACT_ASSERT(cond)
#else
    #define BOOST_CONTRACT_ASSERT_AUDIT(cond) \
        BOOST_CONTRACT_ASSERT(true || (cond))
#endif

#define BOOST_CONTRACT_ASSERT_AXIOM(cond) \
    BOOST_CONTRACT_ASSERT(true || (cond))

Base Types (Variadic)
As shown in Base Classes, this library provides the BOOST_CONTRACT_BASE_TYPES variadic macro to declare the base_types member type that will expand to the list of all public bases for a derived class. Programmers can also declare base_types without using BOOST_CONTRACT_BASE_TYPES at the cost of writing a bit more code and increase maintenance efforts. For example (see base_types_no_macro.cpp):

#include <boost/mpl/vector.hpp>

class chars :
    private boost::contract::constructor_precondition<chars>,
    public unique_chars,
    public virtual pushable<char>,
    virtual protected has_size,
    private has_empty
{
public:
    // Program `base_types` without macros (list only public bases).
    typedef boost::mpl::vector<unique_chars, pushable<char> > base_types;

    /* ... */

The base_types member type must be a boost::mpl::vector which must list all and only public base classes (because only public bases subcontract, see Function Calls), and in the same order these public base classes appear in the derived class inheritance list. If the BOOST_CONTRACT_BASE_TYPES macro is not used, it is the responsibility of the programmers to maintain the correct list of bases in the boost::mpl::vector each time the derived class inheritance list changes (this might significantly complicate maintenance).
In general, it is recommended to use the BOOST_CONTRACT_BASE_TYPES macro whenever possible.

Old Values (Variadic)
As shown in Old Values, this library provides the BOOST_CONTRACT_OLDOF variadic macro to assign old value copies. Programmers can also assign old values without using BOOST_CONTRACT_OLDOF at the cost of writing a bit more code manually. For example (see old_no_macro.cpp):

template<typename T>
class vector {
public:
    virtual void push_back(T const& value, boost::contract::virtual_* v = 0) {
        // Program old value instead of using `OLD(size())` macro.
        boost::contract::old_ptr<unsigned> old_size =
            boost::contract::make_old(v, boost::contract::copy_old(v) ?
                    size() : boost::contract::null_old())
        ;

        boost::contract::check c = boost::contract::public_function(v, this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
            })
        ;

        vect_.push_back(value);
    }

    /* ... */

The ternary operator boost::contract::copy_old(v) ? size() : boost::contract::null_old() must be used here to avoid evaluating and copying the old value expression size() when boost::contract::copy_old returns false (because old values are not being copied when postcondition and exception guarantee checking is disabled at run-time, an overridden virtual function call is not checking postconditions or exception guarantees yet, etc.). The enclosing boost::contract::make_old copies the old value expression and creates an old value pointer. Otherwise, boost::contract::null_old indicates that a null old value pointer should be created.
The boost::contract::make_old and boost::contract::copy_old functions are used exactly as shown above but without the extra v parameter when they are called from within non-virtual functions (see Public Function Overrides). The old value pointer returned by boost::contract::make_old can be assigned to either boost::contract::old_ptr or boost::contract::old_ptr_if_copyable (see Old Value Requirements).
In general, it is recommended to use the BOOST_CONTRACT_OLDOF macro whenever possible.

Macro Interface (Variadic)
Almost all macros defined in boost/contract_macro.hpp are variadic macros. On compilers that do not support variadic macros, programmers can manually disable contract code compilation using #ifndef BOOST_CONTRACT_NO_... statements as shown in Disable Contract Compilation.

Examples
This section lists some examples taken from different sources discussing contract programming and implemented here using this library.
Some of these examples might be from old code, containing obsolete coding practices, not optimized for execution speed, not complete, and they might be more relevant in the context of programming languages different from C++. Nevertheless, programmers are encouraged to review these examples to see a few diverse uses of this library that might be relevant to their needs.
The examples in this sections are taken from the following sources:
[N1962]: Examples from a detailed and complete proposal to add contract programming to C++11 (unfortunately, this proposal was never accepted into the standard).
[Meyer97]: Examples from the Eiffel programming language (reprogrammed here in C++ using this library).
[Mitchell02]: Additional examples from the Eiffel programming language (reprogrammed here in C++ using this library).
[Cline90]: Examples from a very early proposal called Annotated C++ (A++) to add contract programming to C++ (A++ was never implemented or proposed for addition to the standard).
The following are some examples of particular interest:
[N1962] Vector: Complete set of contracts for std::vector, plus a comparison with [N1962] syntax.
[N1962] Square Root: Comparison with D syntax.
[Mitchell02] Counter: Subcontracting.
[Meyer97] Stack4: Comparison with Eiffel syntax.
[Cline90] Vector: Comparison with A++ syntax.
Most of the examples listed here use old values and class invariants which are instead not supported by [P0380]. Therefore, there is not meaningful example here that can be directly implemented and compared using [P0380] syntax.

[N1962] Vector: Contracts for STL vector and comparison with [N1962] proposed syntax
On compilers that support C++17 if constexpr, the following example using this library can be simplified removing boost::contract::condition_if and related functor templates such as all_of_equal_to, etc., making it more similar to the pseudo-code on the right-hand side (see Assertion Requirements).
This library	[N1962] proposal (not accepted in C++) plus C++17 if constexpr
#include <boost/contract.hpp> #include <boost/bind.hpp> #include <boost/optional.hpp> #include <boost/algorithm/cxx11/all_of.hpp> #include <boost/type_traits/has_equal_to.hpp> #include <boost/next_prior.hpp> #include <vector> #include <functional> #include <iterator> #include <memory> #include <cassert> // Could be programmed at call site with C++14 generic lambdas. struct all_of_equal_to { typedef bool result_type; template<typename InputIter, typename T> result_type operator()(InputIter first, InputIter last, T const& value) { return boost::algorithm::all_of_equal(first, last, value); } template<typename InputIter> result_type operator()(InputIter first, InputIter last, InputIter where) { for(InputIter i = first, j = where; i != last; ++i, ++j) { if(*i != *j) return false; } return true; } }; template<typename Iter> bool valid(Iter first, Iter last); // Cannot implement in C++ (for axiom only). template<typename Iter> bool contained(Iter first1, Iter last1, Iter first2, Iter last2); // For axiom. // STL vector requires T copyable but not equality comparable. template<typename T, class Allocator = std::allocator<T> > class vector { friend class boost::contract::access; void invariant() const { BOOST_CONTRACT_ASSERT(empty() == (size() == 0)); BOOST_CONTRACT_ASSERT(std::distance(begin(), end()) == int(size())); BOOST_CONTRACT_ASSERT(std::distance(rbegin(), rend()) == int(size())); BOOST_CONTRACT_ASSERT(size() <= capacity()); BOOST_CONTRACT_ASSERT(capacity() <= max_size()); } public: typedef typename std::vector<T, Allocator>::allocator_type allocator_type; typedef typename std::vector<T, Allocator>::pointer pointer; typedef typename std::vector<T, Allocator>::const_pointer const_pointer; typedef typename std::vector<T, Allocator>::reference reference; typedef typename std::vector<T, Allocator>::const_reference const_reference; typedef typename std::vector<T, Allocator>::value_type value_type; typedef typename std::vector<T, Allocator>::iterator iterator; typedef typename std::vector<T, Allocator>::const_iterator const_iterator; typedef typename std::vector<T, Allocator>::size_type size_type; typedef typename std::vector<T, Allocator>::difference_type difference_type; typedef typename std::vector<T, Allocator>::reverse_iterator reverse_iterator; typedef typename std::vector<T, Allocator>::const_reverse_iterator const_reverse_iterator; vector() : vect_() { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(empty()); }) ; } explicit vector(Allocator const& alloc) : vect_(alloc) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(empty()); BOOST_CONTRACT_ASSERT(get_allocator() == alloc); }) ; } explicit vector(size_type count) : vect_(count) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == count); BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(all_of_equal_to(), begin(), end(), T()) ) ); }) ; } vector(size_type count, T const& value) : vect_(count, value) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == count); BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(all_of_equal_to(), begin(), end(), boost::cref(value)) ) ); }) ; } vector(size_type count, T const& value, Allocator const& alloc) : vect_(count, value, alloc) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == count); BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(all_of_equal_to(), begin(), end(), boost::cref(value)) ) ); BOOST_CONTRACT_ASSERT(get_allocator() == alloc); }) ; } template<typename InputIter> vector(InputIter first, InputIter last) : vect_(first, last) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(std::distance(first, last) == int(size())); }) ; } template<typename InputIter> vector(InputIter first, InputIter last, Allocator const& alloc) : vect_(first, last, alloc) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(std::distance(first, last) == int(size())); BOOST_CONTRACT_ASSERT(get_allocator() == alloc); }) ; } /* implicit */ vector(vector const& other) : vect_(other.vect_) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(std::equal_to<vector<T> >(), boost::cref(*this), boost::cref(other)) ) ); }) ; } vector& operator=(vector const& other) { boost::optional<vector&> result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(std::equal_to<vector<T> >(), boost::cref(*this), boost::cref(other)) ) ); BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(std::equal_to<vector<T> >(), boost::cref(*result), boost::cref(*this)) ) ); }) ; if(this != &other) vect_ = other.vect_; return *(result = *this); } virtual ~vector() { // Check invariants. boost::contract::check c = boost::contract::destructor(this); } void reserve(size_type count) { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(count < max_size()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(capacity() >= count); }) ; vect_.reserve(count); } size_type capacity() const { size_type result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(result >= size()); }) ; return result = vect_.capacity(); } iterator begin() { iterator result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { if(empty()) BOOST_CONTRACT_ASSERT(result == end()); }) ; return result = vect_.begin(); } const_iterator begin() const { const_iterator result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { if(empty()) BOOST_CONTRACT_ASSERT(result == end()); }) ; return result = vect_.begin(); } iterator end() { // Check invariants. boost::contract::check c = boost::contract::public_function(this); return vect_.end(); } const_iterator end() const { // Check invariants. boost::contract::check c = boost::contract::public_function(this); return vect_.end(); } reverse_iterator rbegin() { iterator result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { if(empty()) BOOST_CONTRACT_ASSERT(result == rend()); }) ; return result = vect_.rbegin(); } const_reverse_iterator rbegin() const { const_reverse_iterator result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { if(empty()) BOOST_CONTRACT_ASSERT(result == rend()); }) ; return result = vect_.rbegin(); } reverse_iterator rend() { // Check invariants. boost::contract::check c = boost::contract::public_function(this); return vect_.rend(); } const_reverse_iterator rend() const { // Check invariants. boost::contract::check c = boost::contract::public_function(this); return vect_.rend(); } void resize(size_type count, T const& value = T()) { boost::contract::old_ptr<size_type> old_size = BOOST_CONTRACT_OLDOF(size()); boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == count); if(count > *old_size) { BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(all_of_equal_to(), begin() + *old_size, end(), boost::cref(value)) ) ); } }) ; vect_.resize(count, value); } size_type size() const { size_type result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(result <= capacity()); }) ; return result = vect_.size(); } size_type max_size() const { size_type result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(result >= capacity()); }) ; return result = vect_.max_size(); } bool empty() const { bool result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(result == (size() == 0)); }) ; return result = vect_.empty(); } Allocator get_allocator() const { // Check invariants. boost::contract::check c = boost::contract::public_function(this); return vect_.get_allocator(); } reference at(size_type index) { // Check invariants, no pre (throw out_of_range for invalid index). boost::contract::check c = boost::contract::public_function(this); return vect_.at(index); } const_reference at(size_type index) const { // Check invariants, no pre (throw out_of_range for invalid index). boost::contract::check c = boost::contract::public_function(this); return vect_.at(index); } reference operator[](size_type index) { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(index < size()); }) ; return vect_[index]; } const_reference operator[](size_type index) const { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(index < size()); }) ; return vect_[index]; } reference front() { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(!empty()); }) ; return vect_.front(); } const_reference front() const { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(!empty()); }) ; return vect_.front(); } reference back() { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(!empty()); }) ; return vect_.back(); } const_reference back() const { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(!empty()); }) ; return vect_.back(); } void push_back(T const& value) { boost::contract::old_ptr<size_type> old_size = BOOST_CONTRACT_OLDOF(size()); boost::contract::old_ptr<size_type> old_capacity = BOOST_CONTRACT_OLDOF(capacity()); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(size() < max_size()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == *old_size + 1); BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(std::equal_to<T>(), boost::cref(back()), boost::cref(value)) ) ); }) ; vect_.push_back(value); } void pop_back() { boost::contract::old_ptr<size_type> old_size = BOOST_CONTRACT_OLDOF(size()); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(!empty()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == *old_size - 1); }) ; vect_.pop_back(); } template<typename InputIter> void assign(InputIter first, InputIter last) { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT_AXIOM( !contained(begin(), end(), first, last)); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(std::distance(first, last) == int(size())); }) ; vect_.assign(first, last); } void assign(size_type count, T const& value) { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(count <= max_size()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(all_of_equal_to(), begin(), end(), boost::cref(value)) ) ); }) ; vect_.assign(count, value); } iterator insert(iterator where, T const& value) { iterator result; boost::contract::old_ptr<size_type> old_size = BOOST_CONTRACT_OLDOF(size()); boost::contract::old_ptr<size_type> old_capacity = BOOST_CONTRACT_OLDOF(capacity()); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(size() < max_size()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == *old_size + 1); BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(std::equal_to<T>(), boost::cref(*result), boost::cref(value)) ) ); if(capacity() > *old_capacity) { BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end())); } else { BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end())); } }) ; return result = vect_.insert(where, value); } void insert(iterator where, size_type count, T const& value) { boost::contract::old_ptr<size_type> old_size = BOOST_CONTRACT_OLDOF(size()); boost::contract::old_ptr<size_type> old_capacity = BOOST_CONTRACT_OLDOF(capacity()); boost::contract::old_ptr<iterator> old_where = BOOST_CONTRACT_OLDOF(where); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(size() + count < max_size()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == *old_size + count); BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); if(capacity() == *old_capacity) { BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(all_of_equal_to(), boost::prior(*old_where), boost::prior(*old_where) + count, boost::cref(value) ) ) ); BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end())); } else BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end())); }) ; vect_.insert(where, count, value); } template<typename InputIter> void insert(iterator where, InputIter first, InputIter last) { boost::contract::old_ptr<size_type> old_size = BOOST_CONTRACT_OLDOF(size()); boost::contract::old_ptr<size_type> old_capacity = BOOST_CONTRACT_OLDOF(capacity()); boost::contract::old_ptr<iterator> old_where = BOOST_CONTRACT_OLDOF(where); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(size() + std::distance(first, last) < max_size()); BOOST_CONTRACT_ASSERT_AXIOM( !contained(first, last, begin(), end())); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == *old_size() + std::distance(first, last)); BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); if(capacity() == *old_capacity) { BOOST_CONTRACT_ASSERT( boost::contract::condition_if<boost::has_equal_to<T> >( boost::bind(all_of_equal_to(), first, last, *old_where) ) ); BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end())); } else BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end())); }) ; vect_.insert(where, first, last); } iterator erase(iterator where) { iterator result; boost::contract::old_ptr<size_type> old_size = BOOST_CONTRACT_OLDOF(size()); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(!empty()); BOOST_CONTRACT_ASSERT(where != end()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == *old_size - 1); if(empty()) BOOST_CONTRACT_ASSERT(result == end()); BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end())); }) ; return result = vect_.erase(where); } iterator erase(iterator first, iterator last) { iterator result; boost::contract::old_ptr<size_type> old_size = BOOST_CONTRACT_OLDOF(size()); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(size() >= std::distance(first, last)); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == *old_size - std::distance(first, last)); if(empty()) BOOST_CONTRACT_ASSERT(result == end()); BOOST_CONTRACT_ASSERT_AXIOM(!valid(first, last)); }) ; return result = vect_.erase(first, last); } void clear() { boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(empty()); }) ; vect_.clear(); } void swap(vector& other) { boost::contract::old_ptr<vector> old_me, old_other; #ifdef BOOST_CONTRACT_AUDITS old_me = BOOST_CONTRACT_OLDOF(*this); old_other = BOOST_CONTRACT_OLDOF(other); #endif boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(get_allocator() == other.get_allocator()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT_AUDIT( boost::contract::condition_if<boost::has_equal_to< vector<T> > >( boost::bind(std::equal_to<vector<T> >(), boost::cref(*this), boost::cref(*old_other)) ) ); BOOST_CONTRACT_ASSERT_AUDIT( boost::contract::condition_if<boost::has_equal_to< vector<T> > >( boost::bind(std::equal_to<vector<T> >(), boost::cref(other), boost::cref(*old_me)) ) ); }) ; vect_.swap(other); } friend bool operator==(vector const& left, vector const& right) { // Check class invariants for left and right objects. boost::contract::check left_inv = boost::contract::public_function(&left); boost::contract::check right_inv = boost::contract::public_function(&right); return left.vect_ == right.vect_; } private: std::vector<T, Allocator> vect_; }; int main() { // char type has operator==. vector<char> v(3); assert(v.size() == 3); assert(boost::algorithm::all_of_equal(v, '\0')); vector<char> const& cv = v; assert(cv == v); vector<char> w(v); assert(w == v); typename vector<char>::iterator i = v.begin(); assert(*i == '\0'); typename vector<char>::const_iterator ci = cv.begin(); assert(*ci == '\0'); v.insert(i, 2, 'a'); assert(v[0] == 'a'); assert(v[1] == 'a'); v.push_back('b'); assert(v.back() == 'b'); struct x {}; // x type doest not have operator==. vector<x> y(3); assert(y.size() == 3); vector<x> const& cy = y; vector<x> z(y); typename vector<x>::iterator j = y.begin(); assert(j != y.end()); typename vector<x>::const_iterator cj = cy.begin(); assert(cj != cy.end()); y.insert(j, 2, x()); y.push_back(x()); return 0; }	// Extra spaces, newlines, etc. for visual alignment with this library code. #include <boost/algorithm/cxx11/all_of.hpp> #include <boost/type_traits/has_equal_to.hpp> #include <boost/next_prior.hpp> #include <vector> #include <iterator> #include <memory> template< class T, class Allocator = std::allocator<T> > class vector { invariant { empty() == (size() == 0); std::distance(begin(), end()) == int(size()); std::distance(rbegin(), rend()) == int(size()); size() <= capacity(); capacity() <= max_size(); } public: typedef typename std::vector<T, Allocator>::allocator_type allocator_type; typedef typename std::vector<T, Allocator>::pointer pointer; typedef typename std::vector<T, Allocator>::const_pointer const_pointer; typedef typename std::vector<T, Allocator>::reference reference; typedef typename std::vector<T, Allocator>::const_reference const_reference; typedef typename std::vector<T, Allocator>::value_type value_type; typedef typename std::vector<T, Allocator>::iterator iterator; typedef typename std::vector<T, Allocator>::const_iterator const_iterator; typedef typename std::vector<T, Allocator>::size_type size_type; typedef typename std::vector<T, Allocator>::difference_type difference_type; typedef typename std::vector<T, Allocator>::reverse_iterator reverse_iterator; typedef typename std::vector<T, Allocator>::const_reverse_iterator const_reverse_iterator; vector() postcondition { empty(); } : vect_() {} explicit vector(Allocator const& alloc) postcondition { empty(); get_allocator() == alloc; } : vect_(alloc) {} explicit vector(size_type count) postcondition { size() == count; if constexpr(boost::has_equal_to<T>::value) { boost::algorithm::all_of_equal(begin(), end(), T()); } } : vect_(count) {} vector(size_type count, T const& value) postcondition { size() == count; if constexpr(boost::has_equal_to<T>::value) { boost::algorithm::all_of_equal(begin(), end(), value); } } : vect_(count, value) {} vector(size_type count, T const& value, Allocator const& alloc) postcondition { size() == count; if constexpr(boost::has_equal_to<T>::value) { boost::algorithm::all_of_equal(begin(), end(), value); } get_allocator() == alloc; } : vect_(count, value, alloc) {} template<typename InputIter> vector(InputIter first, InputIter last) postcondition { std::distance(first, last) == int(size()); } : vect_(first, last) {} template<typename InputIter> vector(InputIter first, InputIter last, Allocator const& alloc) postcondition { std::distance(first, last) == int(size()); get_allocator() == alloc; } : vect_(first, last, alloc) {} /* implicit */ vector(vector const& other) postcondition { if constexpr(boost::has_equal_to<T>::value) { *this == other; } } : vect_(other.vect_) {} vector& operator=(vector const& other) postcondition(result) { if constexpr(boost::has_equal_to<T>::value) { *this == other; result == *this; } } { if(this != &other) vect_ = other.vect_; return *this; } virtual ~vector() {} void reserve(size_type count) precondition { count < max_size(); } postcondition { capacity() >= count; } { vect_.reserve(count); } size_type capacity() const postcondition(result) { result >= size(); } { return vect_.capacity(); } iterator begin() postcondition { if(empty()) result == end(); } { return vect_.begin(); } const_iterator begin() const postcondition(result) { if(empty()) result == end(); } { return vect_.begin(); } iterator end() { return vect_.end(); } const_iterator end() const { return vect_.end(); } reverse_iterator rbegin() postcondition(result) { if(empty()) result == rend(); } { return vect_.rbegin(); } const_reverse_iterator rbegin() const postcondition(result) { if(empty()) result == rend(); } { return vect_.rbegin(); } reverse_iterator rend() { return vect_.rend(); } const_reverse_iterator rend() const { return vect_.rend(); } void resize(size_type count, T const& value = T()) postcondition { size() == count; if constexpr(boost::has_equal_to<T>::value) { if(count > oldof(size())) { boost::algorithm::all_of_equal(begin() + oldof(size()), end(), value); } } } { vect_.resize(count, value); } size_type size() const postcondition(result) { result <= capacity(); } { return vect_.size(); } size_type max_size() const postcondition(result) { result >= capacity(); } { return vect_.max_size(); } bool empty() const postcondition(result) { result == (size() == 0); } { return vect_.empty(); } Alloctor get_allocator() const { return vect_.get_allocator(); } reference at(size_type index) { // No precondition (throw out_of_range for invalid index). return vect_.at(index); } const_reference at(size_type index) const { // No precondition (throw out_of_range for invalid index). return vect_.at(index); } reference operator[](size_type index) precondition { index < size(); } { return vect_[index]; } const_reference operator[](size_type index) const precondition { index < size(); } { return vect_[index]; } reference front() precondition { !empty(); } { return vect_.front(); } const_reference front() const precondition { !empty(); } { return vect_.front(); } reference back() precondition { !empty(); } { return vect_.back(); } const_reference back() const precondition { !empty(); } { return vect_.back(); } void push_back(T const& value) precondition { size() < max_size(); } postcondition { size() == oldof(size()) + 1; capacity() >= oldof(capacity()) if constexpr(boost::has_equal_to<T>::value) { back() == value; } } { vect_.push_back(value); } void pop_back() precondition { !empty(); } postcondition { size() == oldof(size()) - 1; } { vect_.pop_back(); } template<typename InputIter> void assign(InputIter first, InputIter last) // Precondition: [begin(), end()) does not contain [first, last). postcondition { std::distance(first, last) == int(size()); } { vect_.assign(first, last); } void assign(size_type count, T const& vallue) precondition { count <= max_size(); } postcondition { if constexpr(boost::has_equal_to<T>::value) { boost::algorithm::all_of_equal(begin(), end(), value); } } { vect_.assign(count, value); } iterator insert(iterator where, T const& value) precondition { size() < max_size(); } postcondition(result) { size() == oldof(size()) + 1; capacity() >= oldof(capacity()); if constexpr(boost::has_equal_to<T>::value) { *result == value; } // if(capacity() > oldof(capacity())) // [begin(), end()) is invalid // else // [where, end()) is invalid } { return vect_.insert(where, value); } void insert(iterator where, size_type count, T const& value) precondition { size() + count < max_size(); } postcondition { size() == oldof(size()) + count; capacity() >= oldof(capacity()); if(capacity() == oldof(capacity())) { if constexpr(boost::has_equal_to<T>::value) { boost::algorithm::all_of_equal(boost::prior(oldof(where)), boost::prior(oldof(where)) + count, value); } // [where, end()) is invalid } // else [begin(), end()) is invalid } { vect_.insert(where, count, value); } template<typename InputIter> void insert(iterator where, Iterator first, Iterator last) precondition { size() + std::distance(first, last) < max_size(); // [first, last) is not contained in [begin(), end()) } postcondition { size() == oldof(size()) + std::distance(first, last); capacity() >= oldof(capacity()); if(capacity() == oldof(capacity())) { if constexpr(boost::has_equal_to<T>::value) { boost::algorithm::all_of_equal(first, last, oldof(where)); } // [where, end()) is invalid } // else [begin(), end()) is invalid } { vect_.insert(where, first, last); } iterator erase(iterator where) precondition { !empty(); where != end(); } postcondition(result) { size() == oldod size() - 1; if(empty()) result == end(); // [where, end()) is invalid } { return vect_.erase(where); } iterator erase(iterator first, iterator last) precondition { size() >= std::distance(first, lasst); } postcondition(result) { size() == oldof(size()) - std::distance(first, last); if(empty()) result == end(); // [first, last) is invalid } { return vect_.erase(first, last); } void clear() postcondition { empty(); } { vect_.clear(); } void swap(vector& other) precondition { get_allocator() == other.get_allocator(); } postcondition { if constexpr(boost::has_equal_to<T>::value) { *this == oldof(other); other == oldof(*this); } } { vect_.swap(other); } friend bool operator==(vector const& left, vector const& right) { // Cannot check class invariants for left and right objects. return left.vect_ == right.vect_; } private: std::vector<T, Allocator> vect_; }; // End.

[N1962] Circle: Subcontracting

#include <boost/contract.hpp>
#include <cassert>

class shape {
public:
    virtual ~shape() {}

    virtual unsigned compute_area(boost::contract::virtual_* v = 0) const = 0;
};

unsigned shape::compute_area(boost::contract::virtual_* v) const {
    unsigned result;
    boost::contract::check c = boost::contract::public_function(v, result, this)
        .postcondition([&] (int const& result) {
            BOOST_CONTRACT_ASSERT(result > 0);
        })
    ;
    assert(false);
    return result;
}

class circle
    #define BASES public shape
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
    #undef BASES

    BOOST_CONTRACT_OVERRIDE(compute_area);

public:
    static int const pi = 3; // Truncated to int from 3.14...

    explicit circle(unsigned a_radius) : radius_(a_radius) {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(radius() == a_radius);
            })
        ;
    }

    virtual unsigned compute_area(boost::contract::virtual_* v = 0) const
            /* override */ {
        unsigned result;
        boost::contract::check c = boost::contract::public_function<
                override_compute_area>(v, result, &circle::compute_area, this)
            .postcondition([&] (unsigned const& result) {
                BOOST_CONTRACT_ASSERT(result == pi * radius() * radius());
            })
        ;

        return result = pi * radius() * radius();
    }

    unsigned radius() const {
        boost::contract::check c = boost::contract::public_function(this);
        return radius_;
    }

private:
    unsigned radius_;
};

int main() {
    circle c(2);
    assert(c.radius() == 2);
    assert(c.compute_area() == 12);
    return 0;
}

[N1962] Factorial: Recursion

#include <boost/contract.hpp>
#include <cassert>

int factorial(int n) {
    int result;
    boost::contract::check c = boost::contract::function()
        .precondition([&] {
            BOOST_CONTRACT_ASSERT(n >= 0); // Non-negative natural number.
            BOOST_CONTRACT_ASSERT(n <= 12); // Max function input.
        })
        .postcondition([&] {
            BOOST_CONTRACT_ASSERT(result >= 1);
            if(n < 2) { // Select assertion.
                BOOST_CONTRACT_ASSERT(result == 1);
            } else {
                // Assertions automatically disabled in other assertions.
                // Therefore, this postcondition can recursively call the
                // function without causing infinite recursion.
                BOOST_CONTRACT_ASSERT_AUDIT(n * factorial(n - 1));
            }
        })
    ;

    return n < 2 ? (result = 1) : (result = n * factorial(n - 1));
}

int main() {
    assert(factorial(4) == 24);
    return 0;
}

[N1962] Equal: Operators

#include <boost/contract.hpp>
#include <cassert>

// Forward declaration because == and != contracts use one another's function.
template<typename T>
bool operator==(T const& left, T const& right);

template<typename T>
bool operator!=(T const& left, T const& right) {
    bool result;
    boost::contract::check c = boost::contract::function()
        .postcondition([&] {
            BOOST_CONTRACT_ASSERT(result == !(left == right));
        })
    ;

    return result = (left.value != right.value);
}

template<typename T>
bool operator==(T const& left, T const& right) {
    bool result;
    boost::contract::check c = boost::contract::function()
        .postcondition([&] {
            BOOST_CONTRACT_ASSERT(result == !(left != right));
        })
    ;

    return result = (left.value == right.value);
}

struct number { int value; };

int main() {
    number n;
    n.value = 123;

    assert((n == n) == true);   // Explicitly call operator==.
    assert((n != n) == false);  // Explicitly call operator!=.

    return 0;
}

[N1962] Sum: Array parameter

#include <boost/contract.hpp>
#include <cassert>

int sum(int count, int* array) {
    int result;
    boost::contract::check c = boost::contract::function()
        .precondition([&] {
            BOOST_CONTRACT_ASSERT(count % 4 == 0);
        })
    ;

    result = 0;
    for(int i = 0; i < count; ++i) result += array[i];
    return result;
}

int main() {
    int a[4] = {1, 2, 3, 4};
    assert(sum(4, a) == 10);
    return 0;
}

[N1962] Square Root: Default parameters and comparison with D syntax
This Library	The D Programming Language
#include <boost/contract.hpp> #include <cmath> #include <cassert> long lsqrt(long x) { long result; boost::contract::check c = boost::contract::function() .precondition([&] { BOOST_CONTRACT_ASSERT(x >= 0); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(result * result <= x); BOOST_CONTRACT_ASSERT((result + 1) * (result + 1) > x); }) ; return result = long(std::sqrt(double(x))); } int main() { assert(lsqrt(4) == 2); return 0; }	// Extra spaces, newlines, etc. for visual alignment with this library code. long lsqrt(long x) in { assert(x >= 0); } out(result) { assert(result * result <= x); assert((result + 1) * (result + 1) > x); } do { return cast(long)std.math.sqrt(cast(real)x); } // End.

[Meyer97] Stack4: Comparison with Eiffel syntax
This Library	The Eiffel Programming Language
// File: stack4.hpp #ifndef STACK4_HPP_ #define STACK4_HPP_ #include <boost/contract.hpp> // Dispenser with LIFO access policy and fixed max capacity. template<typename T> class stack4 #define BASES private boost::contract::constructor_precondition<stack4<T> > : BASES { friend boost::contract::access; typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; #undef BASES void invariant() const { BOOST_CONTRACT_ASSERT(count() >= 0); // Count non-negative. BOOST_CONTRACT_ASSERT(count() <= capacity()); // Count bounded. BOOST_CONTRACT_ASSERT(empty() == (count() == 0)); // Empty if no elem. } public: /* Initialization */ // Allocate static from a maximum of n elements. explicit stack4(int n) : boost::contract::constructor_precondition<stack4>([&] { BOOST_CONTRACT_ASSERT(n >= 0); // Non-negative capacity. }) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(capacity() == n); // Capacity set. }) ; capacity_ = n; count_ = 0; array_ = new T[n]; } // Deep copy via constructor. /* implicit */ stack4(stack4 const& other) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(capacity() == other.capacity()); BOOST_CONTRACT_ASSERT(count() == other.count()); BOOST_CONTRACT_ASSERT_AXIOM(*this == other); }) ; capacity_ = other.capacity_; count_ = other.count_; array_ = new T[other.capacity_]; for(int i = 0; i < other.count_; ++i) array_[i] = other.array_[i]; } // Deep copy via assignment. stack4& operator=(stack4 const& other) { boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(capacity() == other.capacity()); BOOST_CONTRACT_ASSERT(count() == other.count()); BOOST_CONTRACT_ASSERT_AXIOM(*this == other); }) ; delete[] array_; capacity_ = other.capacity_; count_ = other.count_; array_ = new T[other.capacity_]; for(int i = 0; i < other.count_; ++i) array_[i] = other.array_[i]; return *this; } // Destroy this stack. virtual ~stack4() { // Check invariants. boost::contract::check c = boost::contract::destructor(this); delete[] array_; } /* Access */ // Max number of stack elements. int capacity() const { // Check invariants. boost::contract::check c = boost::contract::public_function(this); return capacity_; } // Number of stack elements. int count() const { // Check invariants. boost::contract::check c = boost::contract::public_function(this); return count_; } // Top element. T const& item() const { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(!empty()); // Not empty (i.e., count > 0). }) ; return array_[count_ - 1]; } /* Status Report */ // Is stack empty? bool empty() const { bool result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { // Empty definition. BOOST_CONTRACT_ASSERT(result == (count() == 0)); }) ; return result = (count_ == 0); } // Is stack full? bool full() const { bool result; boost::contract::check c = boost::contract::public_function(this) .postcondition([&] { BOOST_CONTRACT_ASSERT( // Full definition. result == (count() == capacity())); }) ; return result = (count_ == capacity_); } /* Element Change */ // Add x on top. void put(T const& x) { boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(!full()); // Not full. }) .postcondition([&] { BOOST_CONTRACT_ASSERT(!empty()); // Not empty. BOOST_CONTRACT_ASSERT(item() == x); // Added to top. BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // One more. }) ; array_[count_++] = x; } // Remove top element. void remove() { boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(!empty()); // Not empty (i.e., count > 0). }) .postcondition([&] { BOOST_CONTRACT_ASSERT(!full()); // Not full. BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // One less. }) ; --count_; } /* Friend Helpers */ friend bool operator==(stack4 const& left, stack4 const& right) { boost::contract::check inv1 = boost::contract::public_function(&left); boost::contract::check inv2 = boost::contract::public_function(&right); if(left.count_ != right.count_) return false; for(int i = 0; i < left.count_; ++i) { if(left.array_[i] != right.array_[i]) return false; } return true; } private: int capacity_; int count_; T* array_; // Internally use C-style array. }; #endif // #include guard	-- Extra spaces, newlines, etc. for visual alignment with this library code. indexing destription: "Dispenser with LIFO access policy and a fixed max capacity." class interface STACK4[G] creation make -- Interface only (no implementation). invariant count_non_negative: count >= 0 count_bounded: count <= capacity empty_if_no_elements: empty = (count = 0) feature -- Initialization -- Allocate stack for a maximum of n elements. make(n: INTEGER) is require non_negative_capacity: n >= 0 ensure capacity_set: capacity = n end feature -- Access -- Max number of stack elements. capacity: INTEGER -- Number of stack elements. count: INTEGER -- Top element. item: G is require not_empty: not empty -- i.e., count > 0 end feature -- Status report -- Is stack empty? empty: BOOLEAN is ensure empty_definition: result = (count = 0) end -- Is stack full? full: BOOLEAN is ensure full_definition: result = (count = capacity) end feature -- Element change -- Add x on top. put(x: G) is require not_full: not full ensure not_empty: not empty added_to_top: item = x one_more_item: count = old count + 1 end -- Remove top element. remove is require not_empty: not empty -- i.e., count > 0 ensure not_full: not full one_fewer_item: count = old count - 1 end end -- class interface STACK4 -- End.
#include "stack4.hpp" #include <cassert> int main() { stack4<int> s(3); assert(s.capacity() == 3); assert(s.count() == 0); assert(s.empty()); assert(!s.full()); s.put(123); assert(!s.empty()); assert(!s.full()); assert(s.item() == 123); s.remove(); assert(s.empty()); assert(!s.full()); return 0; }

[Meyer97] Stack3: Error codes instead of preconditions

// File: stack3.cpp
#include "stack4.hpp"
#include <boost/contract.hpp>
#include <boost/optional.hpp>
#include <cassert>

// Dispenser LIFO with max capacity using error codes.
template<typename T>
class stack3 {
    friend class boost::contract::access;

    void invariant() const {
        if(!error()) {
            BOOST_CONTRACT_ASSERT(count() >= 0); // Count non-negative.
            BOOST_CONTRACT_ASSERT(count() <= capacity()); // Count bounded.
            // Empty if no element.
            BOOST_CONTRACT_ASSERT(empty() == (count() == 0));
        }
    }

public:
    enum error_code {
        no_error = 0,
        overflow_error,
        underflow_error,
        size_error
    };

    /* Initialization */

    // Create stack for max of n elems, if n < 0 set error (no preconditions).
    explicit stack3(int n, T const& default_value = T()) :
            stack_(0), error_(no_error) {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                // Error if impossible.
                BOOST_CONTRACT_ASSERT((n < 0) == (error() == size_error));
                // No error if possible.
                BOOST_CONTRACT_ASSERT((n >= 0) == !error());
                // Created if no error.
                if(!error()) BOOST_CONTRACT_ASSERT(capacity() == n);
            })
        ;

        if(n >= 0) stack_ = stack4<T>(n);
        else error_ = size_error;
    }

    /* Access */

    // Max number of stack elements.
    int capacity() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return stack_.capacity();
    }

    // Number of stack elements.
    int count() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return stack_.count();
    }

    // Top element if present, otherwise none and set error (no preconditions).
    boost::optional<T const&> item() const {
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // Error if impossible.
                BOOST_CONTRACT_ASSERT(empty() == (error() == underflow_error));
                // No error if possible.
                BOOST_CONTRACT_ASSERT(!empty() == !error());
            })
        ;

        if(!empty()) {
            error_ = no_error;
            return boost::optional<T const&>(stack_.item());
        } else {
            error_ = underflow_error;
            return boost::optional<T const&>();
        }
    }

    /* Status Report */

    // Error indicator set by various operations.
    error_code error() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return error_;
    }

    bool empty() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return stack_.empty();
    }

    bool full() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return stack_.full();
    }

    /* Element Change */

    // Add x to top if capacity allows, otherwise set error (no preconditions).
    void put(T const& x) {
        boost::contract::old_ptr<bool> old_full = BOOST_CONTRACT_OLDOF(full());
        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // Error if impossible.
                BOOST_CONTRACT_ASSERT(*old_full == (error() == overflow_error));
                // No error if possible.
                BOOST_CONTRACT_ASSERT(!*old_full == !error());
                if(!error()) { // If no error...
                    BOOST_CONTRACT_ASSERT(!empty()); // ...not empty.
                    BOOST_CONTRACT_ASSERT(*item() == x); // ...added to top.
                    // ...one more.
                    BOOST_CONTRACT_ASSERT(count() == *old_count + 1);
                }
            })
        ;

        if(full()) error_ = overflow_error;
        else {
            stack_.put(x);
            error_ = no_error;
        }
    }

    // Remove top element if possible, otherwise set error (no preconditions).
    void remove() {
        boost::contract::old_ptr<bool> old_empty =
                BOOST_CONTRACT_OLDOF(empty());
        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // Error if impossible.
                BOOST_CONTRACT_ASSERT(*old_empty == (error() ==
                        underflow_error));
                // No error if possible.
                BOOST_CONTRACT_ASSERT(!*old_empty == !error());
                if(!error()) { // If no error...
                    BOOST_CONTRACT_ASSERT(!full()); // ...not full.
                    // ...one less.
                    BOOST_CONTRACT_ASSERT(count() == *old_count - 1);
                }
            })
        ;

        if(empty()) error_ = underflow_error;
        else {
            stack_.remove();
            error_ = no_error;
        }
    }

private:
    stack4<T> stack_;
    mutable error_code error_;
};

int main() {
    stack3<int> s(3);
    assert(s.capacity() == 3);
    assert(s.count() == 0);
    assert(s.empty());
    assert(!s.full());

    s.put(123);
    assert(!s.empty());
    assert(!s.full());
    assert(*s.item() == 123);

    s.remove();
    assert(s.empty());
    assert(!s.full());

    return 0;
}

[Mitchell02] Name List: Relaxed subcontracts

#include <boost/contract.hpp>
#include <string>
#include <vector>
#include <algorithm>
#include <cassert>

// List of names.
class name_list {
    friend class boost::contract::access;

    void invariant() const {
        BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
    }

public:
    /* Creation */

    // Create an empty list.
    name_list() {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == 0); // Empty list.
            })
        ;
    }

    // Destroy list.
    virtual ~name_list() {
        // Check invariants.
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Basic Queries */

    // Number of names in list.
    int count() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return names_.size();
    }

    // Is name in list?
    bool has(std::string const& name) const {
        bool result;
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // If empty, has not.
                if(count() == 0) BOOST_CONTRACT_ASSERT(!result);
            })
        ;

        return result = names_.cend() != std::find(names_.cbegin(),
                names_.cend(), name);
    }

    /* Commands */

    // Add name to list, if name not already in list.
    virtual void put(std::string const& name,
            boost::contract::virtual_* v = 0) {
        boost::contract::old_ptr<bool> old_has_name =
                BOOST_CONTRACT_OLDOF(v, has(name));
        boost::contract::old_ptr<int> old_count =
                BOOST_CONTRACT_OLDOF(v, count());
        boost::contract::check c = boost::contract::public_function(v, this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(!has(name)); // Not already in list.
            })
            .postcondition([&] {
                if(!*old_has_name) { // If-guard allows to relax subcontracts.
                    BOOST_CONTRACT_ASSERT(has(name)); // Name in list.
                    BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Inc.
                }
            })
        ;

        names_.push_back(name);
    }

private:
    std::vector<std::string> names_;
};

class relaxed_name_list
    #define BASES public name_list
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting.
    #undef BASES

    BOOST_CONTRACT_OVERRIDE(put);

public:
    /*  Commands */

    // Add name to list, or do nothing if name already in list (relaxed).
    void put(std::string const& name,
            boost::contract::virtual_* v = 0) /* override */ {
        boost::contract::old_ptr<bool> old_has_name =
                BOOST_CONTRACT_OLDOF(v, has(name));
        boost::contract::old_ptr<int> old_count =
                BOOST_CONTRACT_OLDOF(v, count());
        boost::contract::check c = boost::contract::public_function<
                override_put>(v, &relaxed_name_list::put, this, name)
            .precondition([&] { // Relax inherited preconditions.
                BOOST_CONTRACT_ASSERT(has(name)); // Already in list.
            })
            .postcondition([&] { // Inherited post. not checked given if-guard.
                if(*old_has_name) {
                    // Count unchanged if name already in list.
                    BOOST_CONTRACT_ASSERT(count() == *old_count);
                }
            })
        ;

        if(!has(name)) name_list::put(name); // Else, do nothing.
    }
};

int main() {
    std::string const js = "John Smith";

    relaxed_name_list rl;
    rl.put(js);
    assert(rl.has(js));
    rl.put(js); // OK, relaxed contracts allow calling this again (do nothing).

    name_list nl;
    nl.put(js);
    assert(nl.has(js));
    // nl.put(js); // Error, contracts do not allow calling this again.

    return 0;
}

[Mitchell02] Dictionary: Key-value map

#include <boost/contract.hpp>
#include <utility>
#include <map>
#include <cassert>

template<typename K, typename T>
class dictionary {
    friend class boost::contract::access;

    void invariant() const {
        BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
    }

public:
    /* Creation */

    // Create empty dictionary.
    dictionary() {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == 0); // Empty.
            })
        ;
    }

    // Destroy dictionary.
    virtual ~dictionary() {
        // Check invariants.
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Basic Queries */

    // Number of key entries.
    int count() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return items_.size();
    }

    // Has entry for key?
    bool has(K const& key) const {
        bool result;
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // Empty has no key.
                if(count() == 0) BOOST_CONTRACT_ASSERT(!result);
            })
        ;

        return result = (items_.find(key) != items_.end());
    }

    // Value for a given key.
    T const& value_for(K const& key) const {
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(has(key)); // Has key.
            })
        ;

        // Find != end because of precondition (no defensive programming).
        return items_.find(key)->second;
    }

    /* Commands */

    // Add value of a given key.
    void put(K const& key, T const& value) {
        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(!has(key)); // Has not key already.
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc.
                BOOST_CONTRACT_ASSERT(has(key)); // Has key.
                // Value set for key.
                BOOST_CONTRACT_ASSERT(value_for(key) == value);
            })
        ;

        items_.insert(std::make_pair(key, value));
    }

    // Remove value for given key.
    void remove(K const& key) {
        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(has(key)); // Has key.
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec.
                BOOST_CONTRACT_ASSERT(!has(key)); // Has not key.
            })
        ;

        items_.erase(key);
    }

private:
    std::map<K, T> items_;
};

int main() {
    std::string const js = "John Smith";

    dictionary<std::string, int> ages;
    assert(!ages.has(js));

    ages.put(js, 23);
    assert(ages.value_for(js) == 23);

    ages.remove(js);
    assert(ages.count() == 0);

    return 0;
}

[Mitchell02] Courier: Subcontracting and static class invariants

#include <boost/contract.hpp>
#include <string>
#include <cassert>

struct package {
    double weight_kg;
    std::string location;
    double accepted_hour;
    double delivered_hour;

    explicit package(
        double _weight_kg,
        std::string const& _location = "",
        double _accepted_hour = 0.0,
        double _delivered_hour = 0.0
    ) :
        weight_kg(_weight_kg),
        location(_location),
        accepted_hour(_accepted_hour),
        delivered_hour(_delivered_hour)
    {}
};

// Courier for package delivery.
class courier
    #define BASES private boost::contract::constructor_precondition<courier>
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
    #undef BASES

    static void static_invariant() {
        // Positive min. insurance.
        BOOST_CONTRACT_ASSERT(min_insurance_usd >= 0.0);
    }

    void invariant() const {
        // Above min. insurance.
        BOOST_CONTRACT_ASSERT(insurance_cover_usd() >= min_insurance_usd);
    }

public:
    static double min_insurance_usd;

    /* Creation */

    // Create courier with specified insurance value.
    explicit courier(double _insurance_cover_usd = min_insurance_usd) :
        boost::contract::constructor_precondition<courier>([&] {
            // Positive insurance.
            BOOST_CONTRACT_ASSERT(_insurance_cover_usd >= 0.0);
        }),
        insurance_cover_usd_(_insurance_cover_usd)
    {
        // Check invariants.
        boost::contract::check c = boost::contract::constructor(this);
    }

    // Destroy courier.
    virtual ~courier() {
        // Check invariants.
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Queries */

    // Return insurance cover.
    double insurance_cover_usd() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return insurance_cover_usd_;
    }

    /* Commands */

    // Deliver package to destination.
    virtual void deliver(
        package& package_delivery,
        std::string const& destination,
        boost::contract::virtual_* v = 0
    ) {
        boost::contract::check c = boost::contract::public_function(v, this)
            .precondition([&] {
                // Within max weight of this delivery.
                BOOST_CONTRACT_ASSERT(package_delivery.weight_kg < 5.0);
            })
            .postcondition([&] {
                // Within max delivery type.
                BOOST_CONTRACT_ASSERT(double(package_delivery.delivered_hour -
                        package_delivery.accepted_hour) <= 3.0);
                // Delivered at destination.
                BOOST_CONTRACT_ASSERT(package_delivery.location == destination);
            })
        ;

        package_delivery.location = destination;
        // Delivery takes 2.5 hours.
        package_delivery.delivered_hour = package_delivery.accepted_hour + 2.5;
    }

private:
    double insurance_cover_usd_;
};

double courier::min_insurance_usd = 10.0e+6;

// Different courier for package delivery.
class different_courier
    #define BASES private boost::contract::constructor_precondition< \
            different_courier>, public courier
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting.
    #undef BASES

    static void static_invariant() {
        BOOST_CONTRACT_ASSERT( // Better insurance amount.
                different_insurance_usd >= courier::min_insurance_usd);
    }

    void invariant() const {
        // Above different insurance value.
        BOOST_CONTRACT_ASSERT(insurance_cover_usd() >= different_insurance_usd);
    }

    BOOST_CONTRACT_OVERRIDE(deliver)

public:
    static double different_insurance_usd;

    /* Creation */

    // Create courier with specified insurance value.
    explicit different_courier(
            double insurance_cover_usd = different_insurance_usd) :
        boost::contract::constructor_precondition<different_courier>([&] {
            // Positive insurance value.
            BOOST_CONTRACT_ASSERT(insurance_cover_usd > 0.0);
        }),
        courier(insurance_cover_usd)
    {
        // Check invariants.
        boost::contract::check c = boost::contract::constructor(this);
    }

    // Destroy courier.
    virtual ~different_courier() {
        // Check invariants.
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Commands */

    virtual void deliver(
        package& package_delivery,
        std::string const& destination,
        boost::contract::virtual_* v = 0
    ) /* override */ {
        boost::contract::check c = boost::contract::public_function<
            override_deliver
        >(v, &different_courier::deliver, this, package_delivery, destination)
            .precondition([&] {
                // Package can weight more (weaker precondition).
                BOOST_CONTRACT_ASSERT(package_delivery.weight_kg <= 8.0);
            })
            .postcondition([&] {
                // Faster delivery (stronger postcondition).
                BOOST_CONTRACT_ASSERT(double(package_delivery.delivered_hour -
                        package_delivery.accepted_hour) <= 2.0);
                // Inherited "delivery at destination" postcondition.
            })
        ;

        package_delivery.location = destination;
        // Delivery takes 0.5 hours.
        package_delivery.delivered_hour = package_delivery.accepted_hour + 0.5;
    }
};

double different_courier::different_insurance_usd = 20.0e+6;

int main() {
    package cups(3.6, "store");
    courier c;
    c.deliver(cups, "home");
    assert(cups.location == "home");

    package desk(7.2, "store");
    different_courier dc;
    dc.deliver(desk, "office");
    assert(desk.location == "office");

    return 0;
}

[Mitchell02] Stack: Stack-like container

#include <boost/contract.hpp>
#include <boost/optional.hpp>
#include <vector>
#include <cassert>

template<typename T>
class stack {
    friend class boost::contract::access;

    void invariant() const {
        BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
    }

public:
    /* Creation */

    // Create empty stack.
    stack() {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == 0); // Empty.
            })
        ;
    }

    // Destroy stack.
    virtual ~stack() {
        // Check invariants.
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Basic Queries */

    // Number of items.
    int count() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return items_.size();
    }

    // Item at index in [1, count()] (as in Eiffel).
    T const& item_at(int index) const {
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(index > 0); // Positive index.
                BOOST_CONTRACT_ASSERT(index <= count()); // Index within count.
            })
        ;

        return items_[index - 1];
    }

    /* Derived Queries */

    // If no items.
    bool is_empty() const {
        bool result;
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // Consistent with count.
                BOOST_CONTRACT_ASSERT(result == (count() == 0));
            })
        ;

        return result = (count() == 0);
    }

    // Top item.
    T const& item() const {
        boost::optional<T const&> result; // Avoid extra construction of T.
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(count() > 0); // Not empty.
            })
            .postcondition([&] {
                // Item on top.
                BOOST_CONTRACT_ASSERT(*result == item_at(count()));
            })
        ;

        return *(result = item_at(count()));
    }

    /* Commands */

    // Push item to the top.
    void put(T const& new_item) {
        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc.
                BOOST_CONTRACT_ASSERT(item() == new_item); // Item set.
            })
        ;

        items_.push_back(new_item);
    }

    // Pop top item.
    void remove() {
        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(count() > 0); // Not empty.
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec.
            })
        ;

        items_.pop_back();
    }

private:
    std::vector<T> items_;
};

int main() {
    stack<int> s;
    assert(s.count() == 0);

    s.put(123);
    assert(s.item() == 123);

    s.remove();
    assert(s.is_empty());

    return 0;
}

[Mitchell02] Simple Queue: Queue-like container and disable old value copies for audit assertions

#include <boost/contract.hpp>
#include <boost/optional.hpp>
#include <vector>
#include <cassert>

template<typename T>
class simple_queue
    #define BASES private boost::contract::constructor_precondition< \
            simple_queue<T> >
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
    #undef BASES

    void invariant() const {
        BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
    }

public:
    /* Creation */

    // Create empty queue.
    explicit simple_queue(int a_capacity) :
        boost::contract::constructor_precondition<simple_queue>([&] {
            BOOST_CONTRACT_ASSERT(a_capacity > 0); // Positive capacity.
        })
    {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                // Capacity set.
                BOOST_CONTRACT_ASSERT(capacity() == a_capacity);
                BOOST_CONTRACT_ASSERT(is_empty()); // Empty.
            })
        ;

        items_.reserve(a_capacity);
    }

    // Destroy queue.
    virtual ~simple_queue() {
        // Check invariants.
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Basic Queries */

    // Items in queue (in their order).
    // (Somewhat exposes implementation but allows to check more contracts.)
    std::vector<T> const& items() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return items_;
    }

    // Max number of items queue can hold.
    int capacity() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return items_.capacity();
    }

    /* Derived Queries */

    // Number of items.
    int count() const {
        int result;
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // Return items count.
                BOOST_CONTRACT_ASSERT(result == int(items().size()));
            })
        ;

        return result = items_.size();
    }

    // Item at head.
    T const& head() const {
        boost::optional<T const&> result;
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(!is_empty()); // Not empty.
            })
            .postcondition([&] {
                // Return item on top.
                BOOST_CONTRACT_ASSERT(*result == items().at(0));
            })
        ;

        return *(result = items_.at(0));
    }

    // If queue contains no item.
    bool is_empty() const {
        bool result;
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                // Consistent with count.
                BOOST_CONTRACT_ASSERT(result == (count() == 0));
            })
        ;

        return result = (items_.size() == 0);
    }

    // If queue has no room for another item.
    bool is_full() const {
        bool result;
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT( // Consistent with size and capacity.
                        result == (capacity() == int(items().size())));
            })
        ;

        return result = (items_.size() == items_.capacity());
    }

    /* Commands */

    // Remove head itme and shift all other items.
    void remove() {
        // Expensive all_equal postcond. and old_items copy might be skipped.
        boost::contract::old_ptr<std::vector<T> > old_items;
            #ifdef BOOST_CONTRACT_AUDIITS
                = BOOST_CONTRACT_OLDOF(items())
            #endif // Else, leave old pointer null...
        ;
        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(!is_empty()); // Not empty.
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec.
                // ...following skipped #ifndef AUDITS.
                if(old_items) all_equal(items(), *old_items, /* shifted = */ 1);
            })
        ;

        items_.erase(items_.begin());
    }

    // Add item to tail.
    void put(T const& item) {
        // Expensive all_equal postcond. and old_items copy might be skipped.
        boost::contract::old_ptr<std::vector<T> > old_items;
            #ifdef BOOST_CONTRACT_AUDITS
                = BOOST_CONTRACT_OLDOF(items())
            #endif // Else, leave old pointer null...
        ;
        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(count() < capacity()); // Room for add.
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc.
                // Second to last item.
                BOOST_CONTRACT_ASSERT(items().at(count() - 1) == item);
                // ...following skipped #ifndef AUDITS.
                if(old_items) all_equal(items(), *old_items);
            })
        ;

        items_.push_back(item);
    }

private:
    // Contract helper.
    static bool all_equal(std::vector<T> const& left,
            std::vector<T> const& right, unsigned offset = 0) {
        boost::contract::check c = boost::contract::function()
            .precondition([&] {
                // Correct offset.
                BOOST_CONTRACT_ASSERT(right.size() == left.size() + offset);
            })
        ;

        for(unsigned i = offset; i < right.size(); ++i) {
            if(left.at(i - offset) != right.at(i)) return false;
        }
        return true;
    }

    std::vector<T> items_;
};

int main() {
    simple_queue<int> q(10);
    q.put(123);
    q.put(456);

    assert(q.capacity() == 10);
    assert(q.head() == 123);

    assert(!q.is_empty());
    assert(!q.is_full());

    std::vector<int> const& items = q.items();
    assert(items.at(0) == 123);
    assert(items.at(1) == 456);

    q.remove();
    assert(q.count() == 1);

    return 0;
}

[Mitchell02] Customer Manager: Contracts instead of defensive programming

#include <boost/contract.hpp>
#include <string>
#include <map>
#include <utility>
#include <cassert>

// Basic customer information.
struct customer_info {
    friend class customer_manager;

    typedef std::string identifier;

    identifier id;

    explicit customer_info(identifier const& _id) :
            id(_id), name_(), address_(), birthday_() {}

private:
    std::string name_;
    std::string address_;
    std::string birthday_;
};

// Manage customers.
class customer_manager {
    friend class boost::contract::access;

    void invariant() const {
        BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
    }

public:
    /* Creation */

    customer_manager() {
        // Check invariants.
        boost::contract::check c = boost::contract::constructor(this);
    }

    virtual ~customer_manager() {
        // Check invariants.
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Basic Queries */

    int count() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return customers_.size();
    }

    bool id_active(customer_info::identifier const& id) const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return customers_.find(id) != customers_.cend();
    }

    /* Derived Queries */

    std::string const& name_for(customer_info::identifier const& id) const {
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(id_active(id)); // Active.
            })
        ;

        // Find != end because of preconditions (no defensive programming).
        return customers_.find(id)->second.name_;
    }

    /* Commands */

    void add(customer_info const& info) {
        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                // Not already active.
                BOOST_CONTRACT_ASSERT(!id_active(info.id));
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc.
                BOOST_CONTRACT_ASSERT(id_active(info.id)); // Activated.
            })
        ;

        customers_.insert(std::make_pair(info.id, customer(info)));
    }

    void set_name(customer_info::identifier const& id,
            std::string const& name) {
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(id_active(id)); // Already active.
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(name_for(id) == name); // Name set.
            })
        ;

        // Find != end because of precondition (no defensive programming).
        customers_.find(id)->second.name_ = name;
    }

private:
    class agent {}; // Customer agent.

    struct customer : customer_info {
        agent managing_agent;
        std::string last_contact;

        explicit customer(customer_info const& info) : customer_info(info),
                managing_agent(), last_contact() {}
    };

    std::map<customer_info::identifier, customer> customers_;
};

int main() {
    customer_manager m;
    customer_info const js("john_smith_123");
    m.add(js);
    m.set_name(js.id, "John Smith");
    assert(m.name_for(js.id) == "John Smith");
    assert(m.count() == 1);
    assert(m.id_active(js.id));
    return 0;
}

[Mitchell02] Observer: Pure virtual functions

#ifndef OBSERVER_HPP_
#define OBSERVER_HPP_

#include <boost/contract.hpp>
#include <cassert>

// Observer.
class observer {
    friend class subject;
public:
    // No inv and no bases so contracts optional if no pre, post, and override.

    /* Creation */

    observer() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::constructor(this);
    }

    virtual ~observer() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Commands */

    // If up-to-date with related subject.
    virtual bool up_to_date_with_subject(boost::contract::virtual_* v = 0)
            const = 0;

    // Update this observer.
    virtual void update(boost::contract::virtual_* v = 0) = 0;
};

bool observer::up_to_date_with_subject(boost::contract::virtual_* v) const {
    boost::contract::check c = boost::contract::public_function(v, this);
    assert(false);
    return false;
}

void observer::update(boost::contract::virtual_* v) {
    boost::contract::check c = boost::contract::public_function(v, this)
        .postcondition([&] {
            BOOST_CONTRACT_ASSERT(up_to_date_with_subject()); // Up-to-date.
        })
    ;
    assert(false);
}

#endif // #include guard

#ifndef SUBJECT_HPP_
#define SUBJECT_HPP_

#include "observer.hpp"
#include <boost/contract.hpp>
#include <vector>
#include <algorithm>
#include <cassert>

// Subject for observer design pattern.
class subject {
    friend class boost::contract::access;

    void invariant() const {
        BOOST_CONTRACT_ASSERT_AUDIT(all_observers_valid(observers())); // Valid.
    }

public:
    /* Creation */

    // Construct subject with no observer.
    subject() {
        // Check invariant.
        boost::contract::check c = boost::contract::constructor(this);
    }

    // Destroy subject.
    virtual ~subject() {
        // Check invariant.
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Queries */

    // If given object is attached.
    bool attached(observer const* ob) const {
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(ob); // Not null.
            })
        ;

        return std::find(observers_.cbegin(), observers_.cend(), ob) !=
                observers_.cend();
    }

    /* Commands */

    // Attach given object as an observer.
    void attach(observer* ob) {
        boost::contract::old_ptr<std::vector<observer const*> > old_observers;
        #ifdef BOOST_CONTRACT_AUDITS
            old_observers = BOOST_CONTRACT_OLDOF(observers());
        #endif
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(ob); // Not null.
                BOOST_CONTRACT_ASSERT(!attached(ob)); // Not already attached.
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(attached(ob)); // Attached.
                // Others not changed (frame rule).
                BOOST_CONTRACT_ASSERT_AUDIT(other_observers_unchanged(
                        *old_observers, observers(), ob));
            })
        ;

        observers_.push_back(ob);
    }

protected:
    // Contracts could have been omitted for protected/private with no pre/post.

    /* Queries */

    // All observers attached to this subject.
    std::vector<observer const*> observers() const {
        std::vector<observer const*> obs;
        for(std::vector<observer*>::const_iterator i = observers_.cbegin();
                i != observers_.cend(); ++i) {
            obs.push_back(*i);
        }
        return obs;
    }

    /* Commands */

    // Update all attached observers.
    void notify() {
        // Protected members use `function` (no inv and no subcontracting).
        boost::contract::check c = boost::contract::function()
            .postcondition([&] {
                // All updated.
                BOOST_CONTRACT_ASSERT_AUDIT(all_observers_updated(observers()));
            })
        ;

        for(std::vector<observer*>::iterator i = observers_.begin();
                i != observers_.end(); ++i) {
            // Class invariants ensure no null pointers in observers but class
            // invariants not checked for non-public functions so assert here.
            assert(*i); // Pointer not null (defensive programming).
            (*i)->update();
        }
    }

private:
    /* Contract Helpers */

    static bool all_observers_valid(std::vector<observer const*> const& obs) {
        for(std::vector<observer const*>::const_iterator i = obs.cbegin();
                i != obs.cend(); ++i) {
            if(!*i) return false;
        }
        return true;
    }

    static bool other_observers_unchanged(
        std::vector<observer const*> const& old_obs,
        std::vector<observer const*> const& new_obs,
        observer const* ob
    ) {
        // Private members use `function` (no inv and no subcontracting).
        boost::contract::check c = boost::contract::function()
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(ob); // Not null.
            })
        ;

        std::vector<observer const*> remaining = new_obs;
        std::remove(remaining.begin(), remaining.end(), ob);

        std::vector<observer const*>::const_iterator remaining_it =
                remaining.begin();
        std::vector<observer const*>::const_iterator old_it = old_obs.begin();
        while(remaining.cend() != remaining_it && old_obs.cend() != old_it) {
            if(*remaining_it != *old_it) return false;
            ++remaining_it;
            ++old_it;
        }
        return true;
    }

    static bool all_observers_updated(std::vector<observer const*> const& obs) {
        for(std::vector<observer const*>::const_iterator i = obs.cbegin();
                i != obs.cend(); ++i) {
            if(!*i) return false;
            if(!(*i)->up_to_date_with_subject()) return false;
        }
        return true;
    }

    std::vector<observer*> observers_;
};

#endif // #include guard

#include "observer/observer.hpp"
#include "observer/subject.hpp"
#include <boost/contract.hpp>
#include <cassert>

int test_state; // For testing only.

// Implement an actual subject.
class concrete_subject
    #define BASES public subject
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting.
    #undef BASES

public:
    typedef int state; // Some state being observed.

    concrete_subject() : state_() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::constructor(this);
    }

    virtual ~concrete_subject() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::destructor(this);
    }

    void set_state(state const& new_state) {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::public_function(this);

        state_ = new_state;
        assert(state_ == test_state);
        notify(); // Notify all observers.
    }

    state get_state() const {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::public_function(this);
        return state_;
    }

private:
    state state_;
};

// Implement an actual observer.
class concrete_observer
    #define BASES public observer
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting.
    #undef BASES

    BOOST_CONTRACT_OVERRIDES(up_to_date_with_subject, update)

public:
    // Create concrete observer.
    explicit concrete_observer(concrete_subject const& subj) :
            subject_(subj), observed_state_() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::constructor(this);
    }

    virtual ~concrete_observer() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::destructor(this);
    }

    // Implement base virtual functions.

    bool up_to_date_with_subject(boost::contract::virtual_* v = 0)
            const /* override */ {
        bool result;
        boost::contract::check c = boost::contract::public_function<
            override_up_to_date_with_subject
        >(v, result, &concrete_observer::up_to_date_with_subject, this);

        return result = true; // For simplicity, assume always up-to-date.
    }

    void update(boost::contract::virtual_* v = 0) /* override */ {
        boost::contract::check c = boost::contract::public_function<
                override_update>(v, &concrete_observer::update, this);

        observed_state_ = subject_.get_state();
        assert(observed_state_ == test_state);
    }

private:
    concrete_subject const& subject_;
    concrete_subject::state observed_state_;
};

int main() {
    concrete_subject subj;
    concrete_observer ob(subj);
    subj.attach(&ob);

    subj.set_state(test_state = 123);
    subj.set_state(test_state = 456);

    return 0;
}

[Mitchell02] Counter: Subcontracting

#ifndef PUSH_BUTTON_HPP_
#define PUSH_BUTTON_HPP_

#include <boost/contract.hpp>
#include <cassert>

class push_button {
public:
    // No inv and no bases so contracts optional if no pre, post, and override.

    /* Creation */

    // Create an enabled button.
    push_button() : enabled_(true) {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(enabled()); // Enabled.
            })
        ;
    }

    // Destroy button.
    virtual ~push_button() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Queries */

    // If button is enabled.
    bool enabled() const {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::public_function(this);
        return enabled_;
    }

    /* Commands */

    // Enable button.
    void enable() {
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(enabled()); // Enabled.
            })
        ;

        enabled_ = true;
    }

    // Disable button.
    void disable() {
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(!enabled()); // Disabled.
            })
        ;

        enabled_ = false;
    }

    // Invoke externally when button clicked.
    virtual void on_bn_clicked(boost::contract::virtual_* v = 0) = 0;

private:
    bool enabled_;
};

void push_button::on_bn_clicked(boost::contract::virtual_* v) {
    boost::contract::check c = boost::contract::public_function(v, this)
        .precondition([&] {
            BOOST_CONTRACT_ASSERT(enabled()); // Enabled.
        })
    ;
    assert(false);
}

#endif // #include guard

#ifndef DECREMENT_BUTTON_HPP_
#define DECREMENT_BUTTON_HPP_

#include "push_button.hpp"
#include "counter.hpp"
#include "../observer/observer.hpp"
#include <boost/contract.hpp>
#include <boost/noncopyable.hpp>

class decrement_button
    #define BASES public push_button, public observer, \
            private boost::noncopyable
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
    #undef BASES

    BOOST_CONTRACT_OVERRIDES(on_bn_clicked, up_to_date_with_subject, update);

public:
    /* Creation */

    explicit decrement_button(counter& a_counter) : counter_(a_counter) {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                // Enable iff positive value.
                BOOST_CONTRACT_ASSERT(enabled() == (a_counter.value() > 0));
            })
        ;
        counter_.attach(this);
    }

    // Destroy button.
    virtual ~decrement_button() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Commands */

    virtual void on_bn_clicked(boost::contract::virtual_* v = 0)
            /* override */ {
        boost::contract::old_ptr<int> old_value =
                BOOST_CONTRACT_OLDOF(v, counter_.value());
        boost::contract::check c = boost::contract::public_function<
            override_on_bn_clicked
        >(v, &decrement_button::on_bn_clicked, this)
            .postcondition([&] {
                // Counter decremented.
                BOOST_CONTRACT_ASSERT(counter_.value() == *old_value - 1);
            })
        ;
        counter_.decrement();
    }

    virtual bool up_to_date_with_subject(boost::contract::virtual_* v = 0)
            const /* override */ {
        bool result;
        boost::contract::check c = boost::contract::public_function<
            override_up_to_date_with_subject
        >(v, result, &decrement_button::up_to_date_with_subject, this);

        return result = true; // For simplicity, assume always up-to-date.
    }

    virtual void update(boost::contract::virtual_* v = 0) /* override */ {
        boost::contract::check c = boost::contract::public_function<
                override_update>(v, &decrement_button::update, this)
            .postcondition([&] {
                // Enabled iff positive value.
                BOOST_CONTRACT_ASSERT(enabled() == (counter_.value() > 0));
            })
        ;

        if(counter_.value() == 0) disable();
        else enable();
    }

private:
    counter& counter_;
};

#endif // #include guard

#ifndef COUNTER_HPP_
#define COUNTER_HPP_

#include "../observer/subject.hpp"
#include <boost/contract.hpp>

class counter
    #define BASES public subject
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
    #undef BASES

public:
    /* Creation */

    // Construct counter with specified value.
    explicit counter(int a_value = 10) : value_(a_value) {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(value() == a_value); // Value set.
            })
        ;
    }

    // Destroy counter.
    virtual ~counter() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Queries */

    // Current counter value.
    int value() const {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::public_function(this);
        return value_;
    }

    /* Commands */

    // Decrement counter value.
    void decrement() {
        boost::contract::old_ptr<int> old_value = BOOST_CONTRACT_OLDOF(value());
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(value() == *old_value - 1); // Decrement.
            })
        ;

        --value_;
        notify(); // Notify all attached observers.
    }

private:
    int value_;
};

#endif // #include guard

#include "counter/counter.hpp"
#include "counter/decrement_button.hpp"
#include "observer/observer.hpp"
#include <cassert>

int test_counter;

class view_of_counter
    #define BASES public observer
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
    #undef BASES

    BOOST_CONTRACT_OVERRIDES(up_to_date_with_subject, update)

public:
    /* Creation */

    // Create view associated with given counter.
    explicit view_of_counter(counter& a_counter) : counter_(a_counter) {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::constructor(this);

        counter_.attach(this);
        assert(counter_.value() == test_counter);
    }

    // Destroy view.
    virtual ~view_of_counter() {
        // Could have omitted contracts here (nothing to check).
        boost::contract::check c = boost::contract::destructor(this);
    }

    /* Commands */

    virtual bool up_to_date_with_subject(boost::contract::virtual_* v = 0)
            const /* override */ {
        bool result;
        boost::contract::check c = boost::contract::public_function<
            override_up_to_date_with_subject
        >(v, result, &view_of_counter::up_to_date_with_subject, this);

        return result = true; // For simplicity, assume always up-to-date.
    }

    virtual void update(boost::contract::virtual_* v = 0) /* override */ {
        boost::contract::check c = boost::contract::public_function<
                override_update>(v, &view_of_counter::update, this);

        assert(counter_.value() == test_counter);
    }

private:
    counter& counter_;
};

int main() {
    counter cnt(test_counter = 1);
    view_of_counter view(cnt);

    decrement_button dec(cnt);
    assert(dec.enabled());

    test_counter--;
    dec.on_bn_clicked();
    assert(!dec.enabled());

    return 0;
}

[Cline90] Vector: Comparison with A++ proposal syntax
This Library	A++ Proposal (never actually implemented)
#ifndef VECTOR_HPP_ #define VECTOR_HPP_ #include <boost/contract.hpp> // NOTE: Incomplete contract assertions, addressing only `size`. template<typename T> class vector #define BASES private boost::contract::constructor_precondition<vector<T> > : BASES { friend class boost::contract::access; typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; #undef BASES void invariant() const { BOOST_CONTRACT_ASSERT(size() >= 0); } public: explicit vector(int count = 10) : boost::contract::constructor_precondition<vector>([&] { BOOST_CONTRACT_ASSERT(count >= 0); }), data_(new T[count]), size_(count) { boost::contract::check c = boost::contract::constructor(this) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == count); }) ; for(int i = 0; i < size_; ++i) data_[i] = T(); } virtual ~vector() { boost::contract::check c = boost::contract::destructor(this); delete[] data_; } int size() const { boost::contract::check c = boost::contract::public_function(this); return size_; // Non-negative result already checked by invariant. } void resize(int count) { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(count >= 0); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == count); }) ; T* slice = new T[count]; for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i]; delete[] data_; data_ = slice; size_ = count; } T& operator[](int index) { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(index >= 0); BOOST_CONTRACT_ASSERT(index < size()); }) ; return data_[index]; } T const& operator[](int index) const { boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(index >= 0); BOOST_CONTRACT_ASSERT(index < size()); }) ; return data_[index]; } private: T* data_; int size_; }; #endif // #include guard	// Extra spaces, newlines, etc. for visual alignment with this library code. template<typename T> class vector { legal: // Class invariants (legal). size() >= 0; public: explicit vector(int count = 10) : data_(new T[count]), size_(count) { for(int i = 0; i < size_; ++i) data_[i] = T(); } virtual ~vector() { delete[] data_; } int size() const { return size_; } void resize(int count) { T* slice = new T[count]; for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i]; delete[] data_; data_ = slice; size_ = count; } T& operator[](int index) { return data_[index]; } T& operator[](int index) const { return data_[index]; } axioms: // Preconditions (require) and postconditions (promise) for each func. [int count; require count >= 0; promise size() == count] vector(count); [int count; require count >= 0; promise size() == count] resize(count); [int index; require index >= 0 && index < size()] (*this)[x]; // Op[]. [int index; require index >= 0 && index < size()] (*this)[x] const; // Op[]. private: T* data_; int size_; }; // End.
#include "vector.hpp" #include <cassert> int main() { vector<int> v (3); assert(v.size() == 3); v[0] = 123; v.resize(2); assert(v[0] == 123); assert(v.size() == 2); return 0; }

[Cline90] Stack: Stack-like container

#include <boost/contract.hpp>
#include <cassert>

// NOTE: Incomplete contract assertions, addressing only `empty` and `full`.
template<typename T>
class stack
    #define BASES private boost::contract::constructor_precondition<stack<T> >
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
    #undef BASES

public:
    explicit stack(int capacity) :
        boost::contract::constructor_precondition<stack>([&] {
            BOOST_CONTRACT_ASSERT(capacity >= 0);
        }),
        data_(new T[capacity]), capacity_(capacity), size_(0)
    {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(empty());
                BOOST_CONTRACT_ASSERT(full() == (capacity == 0));
            })
        ;

        for(int i = 0; i < capacity_; ++i) data_[i] = T();
    }

    virtual ~stack() {
        boost::contract::check c = boost::contract::destructor(this);
        delete[] data_;
    }

    bool empty() const {
        boost::contract::check c = boost::contract::public_function(this);
        return size_ == 0;
    }

    bool full() const {
        boost::contract::check c = boost::contract::public_function(this);
        return size_ == capacity_;
    }

    void push(T const& value) {
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(!full());
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(!empty());
            })
        ;

        data_[size_++] = value;
    }

    T pop() {
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(!empty());
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(!full());
            })
        ;

        return data_[--size_];
    }

private:
    T* data_;
    int capacity_;
    int size_;
};

int main() {
    stack<int> s(3);
    s.push(123);
    assert(s.pop() == 123);
    return 0;
}

[Cline90] Vector-Stack: Subcontracting

#include "vector.hpp"
#include <boost/contract.hpp>
#include <boost/optional.hpp>
#include <cassert>

// NOTE: Incomplete contract assertions, addressing only `empty` and `full`.
template<typename T>
class abstract_stack {
public:
    abstract_stack() {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                // AXIOM as empty() cannot actually be checked here to avoid
                // calling pure virtual function length() during construction).
                BOOST_CONTRACT_ASSERT_AXIOM(empty());
            })
        ;
    }

    virtual ~abstract_stack() {
        boost::contract::check c = boost::contract::destructor(this);
    }

    bool full() const {
        bool result;
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(result == (length() == capacity()));
            })
        ;

        return result = (length() == capacity());
    }

    bool empty() const {
        bool result;
        boost::contract::check c = boost::contract::public_function(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(result = (length() == 0));
            })
        ;

        return result = (length() == 0);
    }

    virtual int length(boost::contract::virtual_* v = 0) const = 0;
    virtual int capacity(boost::contract::virtual_* v = 0) const = 0;

    virtual T const& item(boost::contract::virtual_* v = 0) const = 0;

    virtual void push(T const& value, boost::contract::virtual_* v = 0) = 0;
    virtual T const& pop(boost::contract::virtual_* v = 0) = 0;

    virtual void clear(boost::contract::virtual_* v = 0) = 0;
};

template<typename T>
int abstract_stack<T>::length(boost::contract::virtual_* v) const {
    int result;
    boost::contract::check c = boost::contract::public_function(v, result, this)
        .postcondition([&] (int const& result) {
            BOOST_CONTRACT_ASSERT(result >= 0);
        })
    ;
    assert(false);
    return result;
}

template<typename T>
int abstract_stack<T>::capacity(boost::contract::virtual_* v) const {
    int result;
    boost::contract::check c = boost::contract::public_function(v, result, this)
        .postcondition([&] (int const& result) {
            BOOST_CONTRACT_ASSERT(result >= 0);
        })
    ;
    assert(false);
    return result;
}

template<typename T>
T const& abstract_stack<T>::item(boost::contract::virtual_* v) const {
    boost::optional<T const&> result;
    boost::contract::check c = boost::contract::public_function(v, result, this)
        .precondition([&] {
            BOOST_CONTRACT_ASSERT(!empty());
        })
    ;
    assert(false);
    return *result;
}

template<typename T>
void abstract_stack<T>::push(T const& value, boost::contract::virtual_* v) {
    boost::contract::check c = boost::contract::public_function(v, this)
        .precondition([&] {
            BOOST_CONTRACT_ASSERT(!full());
        })
        .postcondition([&] {
            BOOST_CONTRACT_ASSERT(!empty());
        })
    ;
    assert(false);
}

template<typename T>
T const& abstract_stack<T>::pop(boost::contract::virtual_* v) {
    boost::optional<T const&> result;
    boost::contract::old_ptr<T> old_item = BOOST_CONTRACT_OLDOF(v, item());
    boost::contract::check c = boost::contract::public_function(v, result, this)
        .precondition([&] {
            BOOST_CONTRACT_ASSERT(!empty());
        })
        .postcondition([&] (boost::optional<T const&> const& result) {
            BOOST_CONTRACT_ASSERT(!full());
            BOOST_CONTRACT_ASSERT(*result == *old_item);
        })
    ;
    assert(false);
    return *result;
}

template<typename T>
void abstract_stack<T>::clear(boost::contract::virtual_* v) {
    boost::contract::check c = boost::contract::public_function(v, this)
        .postcondition([&] {
            BOOST_CONTRACT_ASSERT(empty());
        })
    ;
    assert(false);
}

template<typename T>
class vstack
    #define BASES private boost::contract::constructor_precondition< \
            vstack<T> >, public abstract_stack<T>
    : BASES
{
    friend class boost::contract::access;

    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
    #undef BASES

    void invariant() const {
        BOOST_CONTRACT_ASSERT(length() >= 0);
        BOOST_CONTRACT_ASSERT(length() < capacity());
    }

    BOOST_CONTRACT_OVERRIDES(length, capacity, item, push, pop, clear)

public:
    explicit vstack(int count = 10) :
        boost::contract::constructor_precondition<vstack>([&] {
            BOOST_CONTRACT_ASSERT(count >= 0);
        }),
        vect_(count), // OK, executed after precondition so count >= 0.
        len_(0)
    {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(length() == 0);
                BOOST_CONTRACT_ASSERT(capacity() == count);
            })
        ;
    }

    virtual ~vstack() {
        boost::contract::check c = boost::contract::destructor(this);
    }

    // Inherited from abstract_stack.

    virtual int length(boost::contract::virtual_* v = 0) const /* override */ {
        int result;
        boost::contract::check c = boost::contract::public_function<
                override_length>(v, result, &vstack::length, this);
        return result = len_;
    }

    virtual int capacity(boost::contract::virtual_* v = 0)
            const /* override */ {
        int result;
        boost::contract::check c = boost::contract::public_function<
                override_capacity>(v, result, &vstack::capacity, this);
        return result = vect_.size();
    }

    virtual T const& item(boost::contract::virtual_* v = 0)
            const /* override */ {
        boost::optional<T const&> result;
        boost::contract::check c = boost::contract::public_function<
                override_item>(v, result, &vstack::item, this);
        return *(result = vect_[len_ - 1]);
    }

    virtual void push(T const& value, boost::contract::virtual_* v = 0)
            /* override */ {
        boost::contract::check c = boost::contract::public_function<
                override_push>(v, &vstack::push, this, value);
        vect_[len_++] = value;
    }

    virtual T const& pop(boost::contract::virtual_* v = 0) /* override */ {
        boost::optional<T const&> result;
        boost::contract::check c = boost::contract::public_function<
                override_pop>(v, result, &vstack::pop, this);
        return *(result = vect_[--len_]);
    }

    virtual void clear(boost::contract::virtual_* v = 0) /* override */ {
        boost::contract::check c = boost::contract::public_function<
                override_clear>(v, &vstack::clear, this);
        len_ = 0;
    }

private:
    vector<T> vect_;
    int len_;
};

int main() {
    vstack<int> s(3);
    assert(s.capacity() == 3);

    s.push(123);
    assert(s.length() == 1);
    assert(s.pop() == 123);

    return 0;
}

[Cline90] Calendar: A very simple calendar

#include <boost/contract.hpp>
#include <cassert>

class calendar {
    friend class boost::contract::access;

    void invariant() const {
        BOOST_CONTRACT_ASSERT(month() >= 1);
        BOOST_CONTRACT_ASSERT(month() <= 12);
        BOOST_CONTRACT_ASSERT(date() >= 1);
        BOOST_CONTRACT_ASSERT(date() <= days_in(month()));
    }

public:
    calendar() : month_(1), date_(31) {
        boost::contract::check c = boost::contract::constructor(this)
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(month() == 1);
                BOOST_CONTRACT_ASSERT(date() == 31);
            })
        ;
    }

    virtual ~calendar() {
        // Check invariants.
        boost::contract::check c = boost::contract::destructor(this);
    }

    int month() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return month_;
    }

    int date() const {
        // Check invariants.
        boost::contract::check c = boost::contract::public_function(this);
        return date_;
    }

    void reset(int new_month) {
        boost::contract::check c = boost::contract::public_function(this)
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(new_month >= 1);
                BOOST_CONTRACT_ASSERT(new_month <= 12);
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(month() == new_month);
            })
        ;

        month_ = new_month;
    }

private:
    static int days_in(int month) {
        int result;
        boost::contract::check c = boost::contract::function()
            .precondition([&] {
                BOOST_CONTRACT_ASSERT(month >= 1);
                BOOST_CONTRACT_ASSERT(month <= 12);
            })
            .postcondition([&] {
                BOOST_CONTRACT_ASSERT(result >= 1);
                BOOST_CONTRACT_ASSERT(result <= 31);
            })
        ;

        return result = 31; // For simplicity, assume all months have 31 days.
    }

    int month_, date_;
};

int main() {
    calendar cal;
    assert(cal.date() == 31);
    assert(cal.month() == 1);

    cal.reset(8); // Set month 
    assert(cal.month() == 8);

    return 0;
}