Adding upstream version 16.2.11+ds.upstream/16.2.11+dsupstream

Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>

8 files changed, 1715 insertions, 0 deletions

diff --git a/src/boost/libs/contract/example/n1962/circle.cpp b/src/boost/libs/contract/example/n1962/circle.cpp
new file mode 100644
index 000000000..21f9345c5
--- /dev/null
+++ b/src/boost/libs/contract/example/n1962/circle.cpp
@@ -0,0 +1,80 @@
+
+// Copyright (C) 2008-2018 Lorenzo Caminiti
+// Distributed under the Boost Software License, Version 1.0 (see accompanying
+// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
+
+//[n1962_circle
+#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;
+}
+//]
+
diff --git a/src/boost/libs/contract/example/n1962/equal.cpp b/src/boost/libs/contract/example/n1962/equal.cpp
new file mode 100644
index 000000000..c1706023a
--- /dev/null
+++ b/src/boost/libs/contract/example/n1962/equal.cpp
@@ -0,0 +1,51 @@
+
+// Copyright (C) 2008-2018 Lorenzo Caminiti
+// Distributed under the Boost Software License, Version 1.0 (see accompanying
+// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
+
+//[n1962_equal
+#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;
+}
+//]
+
diff --git a/src/boost/libs/contract/example/n1962/factorial.cpp b/src/boost/libs/contract/example/n1962/factorial.cpp
new file mode 100644
index 000000000..98f12a38b
--- /dev/null
+++ b/src/boost/libs/contract/example/n1962/factorial.cpp
@@ -0,0 +1,39 @@
+
+// Copyright (C) 2008-2018 Lorenzo Caminiti
+// Distributed under the Boost Software License, Version 1.0 (see accompanying
+// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
+
+//[n1962_factorial
+#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;
+}
+//]
+
diff --git a/src/boost/libs/contract/example/n1962/sqrt.cpp b/src/boost/libs/contract/example/n1962/sqrt.cpp
new file mode 100644
index 000000000..52ade36bb
--- /dev/null
+++ b/src/boost/libs/contract/example/n1962/sqrt.cpp
@@ -0,0 +1,32 @@
+
+// Copyright (C) 2008-2018 Lorenzo Caminiti
+// Distributed under the Boost Software License, Version 1.0 (see accompanying
+// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
+
+//[n1962_sqrt
+#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;
+}
+//]
+
diff --git a/src/boost/libs/contract/example/n1962/sqrt.d b/src/boost/libs/contract/example/n1962/sqrt.d
new file mode 100644
index 000000000..3c550c86e
--- /dev/null
+++ b/src/boost/libs/contract/example/n1962/sqrt.d
@@ -0,0 +1,33 @@
+
+// Copyright (C) 2008-2018 Lorenzo Caminiti
+// Distributed under the Boost Software License, Version 1.0 (see accompanying
+// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
+
+//[n1962_sqrt_d
+// 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.
+//]
+
diff --git a/src/boost/libs/contract/example/n1962/sum.cpp b/src/boost/libs/contract/example/n1962/sum.cpp
new file mode 100644
index 000000000..068619ae9
--- /dev/null
+++ b/src/boost/libs/contract/example/n1962/sum.cpp
@@ -0,0 +1,30 @@
+
+// Copyright (C) 2008-2018 Lorenzo Caminiti
+// Distributed under the Boost Software License, Version 1.0 (see accompanying
+// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
+
+//[n1962_sum
+#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;
+}
+//]
+
diff --git a/src/boost/libs/contract/example/n1962/vector.cpp b/src/boost/libs/contract/example/n1962/vector.cpp
new file mode 100644
index 000000000..bd06c5a7f
--- /dev/null
+++ b/src/boost/libs/contract/example/n1962/vector.cpp
@@ -0,0 +1,725 @@
+
+// Copyright (C) 2008-2018 Lorenzo Caminiti
+// Distributed under the Boost Software License, Version 1.0 (see accompanying
+// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
+
+//[n1962_vector
+#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;
+}
+//]
+
diff --git a/src/boost/libs/contract/example/n1962/vector_n1962.hpp b/src/boost/libs/contract/example/n1962/vector_n1962.hpp
new file mode 100644
index 000000000..2ea88df21
--- /dev/null
+++ b/src/boost/libs/contract/example/n1962/vector_n1962.hpp
@@ -0,0 +1,725 @@
+
+// Copyright (C) 2008-2018 Lorenzo Caminiti
+// Distributed under the Boost Software License, Version 1.0 (see accompanying
+// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
+
+//[n1962_vector_n1962
+// 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.
+//]
+