Boost C++ Libraries Home Libraries People FAQ More

PrevUpHomeNext

Examples

[N1962] Vector: Contracts for STL vector and comparison with [N1962] proposed syntax
[N1962] Circle: Subcontracting
[N1962] Factorial: Recursion
[N1962] Equal: Operators
[N1962] Sum: Array parameter
[N1962] Square Root: Default parameters and comparison with D syntax
[Meyer97] Stack4: Comparison with Eiffel syntax
[Meyer97] Stack3: Error codes instead of preconditions
[Mitchell02] Name List: Relaxed subcontracts
[Mitchell02] Dictionary: Key-value map
[Mitchell02] Courier: Subcontracting and static class invariants
[Mitchell02] Stack: Stack-like container
[Mitchell02] Simple Queue: Queue-like container and disable old value copies for audit assertions
[Mitchell02] Customer Manager: Contracts instead of defensive programming
[Mitchell02] Observer: Pure virtual functions
[Mitchell02] Counter: Subcontracting
[Cline90] Vector: Comparison with A++ proposal syntax
[Cline90] Stack: Stack-like container
[Cline90] Vector-Stack: Subcontracting
[Cline90] Calendar: A very simple calendar

This section lists some examples taken from different sources discussing contract programming and implemented here using this library.

[Note] Note

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:

The following are some examples of particular interest:

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.

#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;
}

#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;
}

#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;
}

#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;
}

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.

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

// 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;
}

#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;
}

#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;
}

#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;
}

#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;
}

#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;
}

#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;
}

#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;
}

#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;
}

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

#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;
}

#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;
}

#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;
}


PrevUpHomeNext