diff options
Diffstat (limited to 'src/boost/libs/contract/example/n1962')
| -rw-r--r-- | src/boost/libs/contract/example/n1962/circle.cpp | 80 | ||||
| -rw-r--r-- | src/boost/libs/contract/example/n1962/equal.cpp | 51 | ||||
| -rw-r--r-- | src/boost/libs/contract/example/n1962/factorial.cpp | 39 | ||||
| -rw-r--r-- | src/boost/libs/contract/example/n1962/sqrt.cpp | 32 | ||||
| -rw-r--r-- | src/boost/libs/contract/example/n1962/sqrt.d | 33 | ||||
| -rw-r--r-- | src/boost/libs/contract/example/n1962/sum.cpp | 30 | ||||
| -rw-r--r-- | src/boost/libs/contract/example/n1962/vector.cpp | 725 | ||||
| -rw-r--r-- | src/boost/libs/contract/example/n1962/vector_n1962.hpp | 725 |
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. +//] + |