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

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