diff options
Diffstat (limited to 'src/boost/libs/contract/example')
74 files changed, 8908 insertions, 0 deletions
diff --git a/src/boost/libs/contract/example/Jamfile.v2 b/src/boost/libs/contract/example/Jamfile.v2 new file mode 100644 index 000000000..3fe6e2fa0 --- /dev/null +++ b/src/boost/libs/contract/example/Jamfile.v2 @@ -0,0 +1,91 @@ + +# 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 + +import ../build/boost_contract_build ; +import ../../config/checks/config : requires ; + +test-suite features : + [ boost_contract_build.subdir-run features : introduction_comments ] + [ boost_contract_build.subdir-run-cxx11 features : introduction ] + [ boost_contract_build.subdir-run-cxx11 features : introduction_public ] + + [ boost_contract_build.subdir-run-cxx11 features : non_member ] + [ boost_contract_build.subdir-run-cxx11 features : lambda ] + [ boost_contract_build.subdir-run-cxx11 features : loop ] + [ boost_contract_build.subdir-run-cxx11 features : code_block ] + [ boost_contract_build.subdir-run-cxx11 features : public ] + [ boost_contract_build.subdir-run-cxx11 features : base_types ] + [ boost_contract_build.subdir-run-cxx11 features : static_public ] + [ boost_contract_build.subdir-run-cxx11 features : private_protected ] + [ boost_contract_build.subdir-run-cxx11 features : + private_protected_virtual ] + [ boost_contract_build.subdir-run-cxx11 features : + private_protected_virtual_multi ] + [ boost_contract_build.subdir-run-cxx11 features : check ] + + [ boost_contract_build.subdir-run-cxx11 features : friend ] + [ boost_contract_build.subdir-run-cxx11 features : friend_invariant ] + [ boost_contract_build.subdir-run-cxx11 features : old ] + [ boost_contract_build.subdir-run-cxx11 features : optional_result ] + [ boost_contract_build.subdir-run-cxx11 features : optional_result_virtual ] + [ boost_contract_build.subdir-run-cxx11 features : pure_virtual_public ] + [ boost_contract_build.subdir-run-cxx11 features : overload ] + [ boost_contract_build.subdir-run-cxx11 features : named_override ] + [ boost_contract_build.subdir-run-cxx11 features : move ] + [ boost_contract_build.subdir-run-cxx11 features : union ] + [ boost_contract_build.subdir-run features : volatile ] + + [ boost_contract_build.subdir-run-cxx11 features : old_if_copyable ] + [ boost_contract_build.subdir-run-cxx11 features : if_constexpr : + [ requires cxx17_if_constexpr ] ] + [ boost_contract_build.subdir-run-cxx11 features : condition_if ] + [ boost_contract_build.subdir-run-cxx11 features : call_if_cxx14 : + [ requires cxx14_generic_lambdas ] ] + [ boost_contract_build.subdir-run-cxx11 features : access ] + [ boost_contract_build.subdir-run-cxx11 features : separate_body ] + [ boost_contract_build.subdir-run-cxx11 features : throw_on_failure ] + [ boost_contract_build.subdir-run-cxx11 features : ifdef ] + [ boost_contract_build.subdir-run-cxx11 features : assertion_level ] + [ boost_contract_build.subdir-run-cxx11 features : ifdef_macro ] + [ boost_contract_build.subdir-run-cxx11 features : base_types_no_macro ] + [ boost_contract_build.subdir-run-cxx11 features : old_no_macro ] + # Still needs C++11 for OLDOF variadic macros. + [ boost_contract_build.subdir-run-cxx11 features : no_lambdas ] + [ boost_contract_build.subdir-run-cxx11 features : no_lambdas_local_func ] +; + +test-suite n1962 : + [ boost_contract_build.subdir-run-cxx11 n1962 : vector ] + [ boost_contract_build.subdir-run-cxx11 n1962 : sqrt ] + [ boost_contract_build.subdir-run-cxx11 n1962 : circle ] + [ boost_contract_build.subdir-run-cxx11 n1962 : equal ] + [ boost_contract_build.subdir-run-cxx11 n1962 : factorial ] + [ boost_contract_build.subdir-run-cxx11 n1962 : sum ] +; + +test-suite meyer97 : + [ boost_contract_build.subdir-run-cxx11 meyer97 : stack4_main ] + [ boost_contract_build.subdir-run-cxx11 meyer97 : stack3 ] +; + +test-suite mitchell02 : + [ boost_contract_build.subdir-run-cxx11 mitchell02 : stack ] + [ boost_contract_build.subdir-run-cxx11 mitchell02 : simple_queue ] + [ boost_contract_build.subdir-run-cxx11 mitchell02 : dictionary ] + [ boost_contract_build.subdir-run-cxx11 mitchell02 : customer_manager ] + [ boost_contract_build.subdir-run-cxx11 mitchell02 : name_list ] + [ boost_contract_build.subdir-run-cxx11 mitchell02 : courier ] + [ boost_contract_build.subdir-run-cxx11 mitchell02 : observer_main ] + [ boost_contract_build.subdir-run-cxx11 mitchell02 : counter_main ] +; + +test-suite cline90 : + [ boost_contract_build.subdir-run-cxx11 cline90 : stack ] + [ boost_contract_build.subdir-run-cxx11 cline90 : vector_main ] + [ boost_contract_build.subdir-run-cxx11 cline90 : vstack ] + [ boost_contract_build.subdir-run-cxx11 cline90 : calendar ] +; + diff --git a/src/boost/libs/contract/example/cline90/calendar.cpp b/src/boost/libs/contract/example/cline90/calendar.cpp new file mode 100644 index 000000000..1dc76ca1e --- /dev/null +++ b/src/boost/libs/contract/example/cline90/calendar.cpp @@ -0,0 +1,93 @@ + +// 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 + +//[cline90_calendar +#include <boost/contract.hpp> +#include <cassert> + +class calendar { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(month() >= 1); + BOOST_CONTRACT_ASSERT(month() <= 12); + BOOST_CONTRACT_ASSERT(date() >= 1); + BOOST_CONTRACT_ASSERT(date() <= days_in(month())); + } + +public: + calendar() : month_(1), date_(31) { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(month() == 1); + BOOST_CONTRACT_ASSERT(date() == 31); + }) + ; + } + + virtual ~calendar() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + int month() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return month_; + } + + int date() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return date_; + } + + void reset(int new_month) { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(new_month >= 1); + BOOST_CONTRACT_ASSERT(new_month <= 12); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(month() == new_month); + }) + ; + + month_ = new_month; + } + +private: + static int days_in(int month) { + int result; + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(month >= 1); + BOOST_CONTRACT_ASSERT(month <= 12); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(result >= 1); + BOOST_CONTRACT_ASSERT(result <= 31); + }) + ; + + return result = 31; // For simplicity, assume all months have 31 days. + } + + int month_, date_; +}; + +int main() { + calendar cal; + assert(cal.date() == 31); + assert(cal.month() == 1); + + cal.reset(8); // Set month + assert(cal.month() == 8); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/cline90/stack.cpp b/src/boost/libs/contract/example/cline90/stack.cpp new file mode 100644 index 000000000..b02c844fe --- /dev/null +++ b/src/boost/libs/contract/example/cline90/stack.cpp @@ -0,0 +1,93 @@ + +// 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 + +//[cline90_stack +#include <boost/contract.hpp> +#include <cassert> + +// NOTE: Incomplete contract assertions, addressing only `empty` and `full`. +template<typename T> +class stack + #define BASES private boost::contract::constructor_precondition<stack<T> > + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + +public: + explicit stack(int capacity) : + boost::contract::constructor_precondition<stack>([&] { + BOOST_CONTRACT_ASSERT(capacity >= 0); + }), + data_(new T[capacity]), capacity_(capacity), size_(0) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(empty()); + BOOST_CONTRACT_ASSERT(full() == (capacity == 0)); + }) + ; + + for(int i = 0; i < capacity_; ++i) data_[i] = T(); + } + + virtual ~stack() { + boost::contract::check c = boost::contract::destructor(this); + delete[] data_; + } + + bool empty() const { + boost::contract::check c = boost::contract::public_function(this); + return size_ == 0; + } + + bool full() const { + boost::contract::check c = boost::contract::public_function(this); + return size_ == capacity_; + } + + void push(T const& value) { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!full()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!empty()); + }) + ; + + data_[size_++] = value; + } + + T pop() { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!empty()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!full()); + }) + ; + + return data_[--size_]; + } + +private: + T* data_; + int capacity_; + int size_; +}; + +int main() { + stack<int> s(3); + s.push(123); + assert(s.pop() == 123); + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/cline90/vector.hpp b/src/boost/libs/contract/example/cline90/vector.hpp new file mode 100644 index 000000000..6e7126217 --- /dev/null +++ b/src/boost/libs/contract/example/cline90/vector.hpp @@ -0,0 +1,101 @@ + +// 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 + +//[cline90_vector +#ifndef VECTOR_HPP_ +#define VECTOR_HPP_ + +#include <boost/contract.hpp> + +// NOTE: Incomplete contract assertions, addressing only `size`. +template<typename T> +class vector + #define BASES private boost::contract::constructor_precondition<vector<T> > + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + void invariant() const { + BOOST_CONTRACT_ASSERT(size() >= 0); + } + +public: + explicit vector(int count = 10) : + boost::contract::constructor_precondition<vector>([&] { + BOOST_CONTRACT_ASSERT(count >= 0); + }), + data_(new T[count]), + size_(count) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(size() == count); + }) + ; + + for(int i = 0; i < size_; ++i) data_[i] = T(); + } + + virtual ~vector() { + boost::contract::check c = boost::contract::destructor(this); + delete[] data_; + } + + int size() const { + boost::contract::check c = boost::contract::public_function(this); + return size_; // Non-negative result already checked by invariant. + } + + void resize(int count) { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(count >= 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(size() == count); + }) + ; + + T* slice = new T[count]; + for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i]; + delete[] data_; + data_ = slice; + size_ = count; + } + + T& operator[](int index) { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(index >= 0); + BOOST_CONTRACT_ASSERT(index < size()); + }) + ; + + return data_[index]; + } + + T const& operator[](int index) const { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(index >= 0); + BOOST_CONTRACT_ASSERT(index < size()); + }) + ; + + return data_[index]; + } + +private: + T* data_; + int size_; +}; + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/cline90/vector_axx.hpp b/src/boost/libs/contract/example/cline90/vector_axx.hpp new file mode 100644 index 000000000..4a3582e61 --- /dev/null +++ b/src/boost/libs/contract/example/cline90/vector_axx.hpp @@ -0,0 +1,101 @@ + +// 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 + +//[cline90_vector_axx +// Extra spaces, newlines, etc. for visual alignment with this library code. + + + + + +template<typename T> +class vector { + + + + + + + + +legal: // Class invariants (legal). + size() >= 0; + + +public: + explicit vector(int count = 10) : + data_(new T[count]), + size_(count) + { + for(int i = 0; i < size_; ++i) data_[i] = T(); + } + + + + + + + + + + + virtual ~vector() { delete[] data_; } + + + + + int size() const { return size_; } + + + + + void resize(int count) { + T* slice = new T[count]; + for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i]; + delete[] data_; + data_ = slice; + size_ = count; + } + + + + + + + + + + + T& operator[](int index) { return data_[index]; } + + + + + + + + + + + T& operator[](int index) const { return data_[index]; } + + + + +axioms: // Preconditions (require) and postconditions (promise) for each func. + [int count; require count >= 0; promise size() == count] vector(count); + [int count; require count >= 0; promise size() == count] resize(count); + [int index; require index >= 0 && index < size()] (*this)[x]; // Op[]. + [int index; require index >= 0 && index < size()] (*this)[x] const; // Op[]. + +private: + T* data_; + int size_; +}; + +// End. +//] + diff --git a/src/boost/libs/contract/example/cline90/vector_main.cpp b/src/boost/libs/contract/example/cline90/vector_main.cpp new file mode 100644 index 000000000..28fa3e91a --- /dev/null +++ b/src/boost/libs/contract/example/cline90/vector_main.cpp @@ -0,0 +1,23 @@ + +// 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 + +//[cline90_vector_main +#include "vector.hpp" +#include <cassert> + +int main() { + vector<int> v (3); + assert(v.size() == 3); + + v[0] = 123; + v.resize(2); + assert(v[0] == 123); + assert(v.size() == 2); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/cline90/vstack.cpp b/src/boost/libs/contract/example/cline90/vstack.cpp new file mode 100644 index 000000000..b210d40aa --- /dev/null +++ b/src/boost/libs/contract/example/cline90/vstack.cpp @@ -0,0 +1,239 @@ + +// 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 + +//[cline90_vstack +#include "vector.hpp" +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <cassert> + +// NOTE: Incomplete contract assertions, addressing only `empty` and `full`. +template<typename T> +class abstract_stack { +public: + abstract_stack() { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + // AXIOM as empty() cannot actually be checked here to avoid + // calling pure virtual function length() during construction). + BOOST_CONTRACT_ASSERT_AXIOM(empty()); + }) + ; + } + + virtual ~abstract_stack() { + boost::contract::check c = boost::contract::destructor(this); + } + + bool full() const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(result == (length() == capacity())); + }) + ; + + return result = (length() == capacity()); + } + + bool empty() const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(result = (length() == 0)); + }) + ; + + return result = (length() == 0); + } + + virtual int length(boost::contract::virtual_* v = 0) const = 0; + virtual int capacity(boost::contract::virtual_* v = 0) const = 0; + + virtual T const& item(boost::contract::virtual_* v = 0) const = 0; + + virtual void push(T const& value, boost::contract::virtual_* v = 0) = 0; + virtual T const& pop(boost::contract::virtual_* v = 0) = 0; + + virtual void clear(boost::contract::virtual_* v = 0) = 0; +}; + +template<typename T> +int abstract_stack<T>::length(boost::contract::virtual_* v) const { + int result; + boost::contract::check c = boost::contract::public_function(v, result, this) + .postcondition([&] (int const& result) { + BOOST_CONTRACT_ASSERT(result >= 0); + }) + ; + assert(false); + return result; +} + +template<typename T> +int abstract_stack<T>::capacity(boost::contract::virtual_* v) const { + int result; + boost::contract::check c = boost::contract::public_function(v, result, this) + .postcondition([&] (int const& result) { + BOOST_CONTRACT_ASSERT(result >= 0); + }) + ; + assert(false); + return result; +} + +template<typename T> +T const& abstract_stack<T>::item(boost::contract::virtual_* v) const { + boost::optional<T const&> result; + boost::contract::check c = boost::contract::public_function(v, result, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!empty()); + }) + ; + assert(false); + return *result; +} + +template<typename T> +void abstract_stack<T>::push(T const& value, boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!full()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!empty()); + }) + ; + assert(false); +} + +template<typename T> +T const& abstract_stack<T>::pop(boost::contract::virtual_* v) { + boost::optional<T const&> result; + boost::contract::old_ptr<T> old_item = BOOST_CONTRACT_OLDOF(v, item()); + boost::contract::check c = boost::contract::public_function(v, result, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!empty()); + }) + .postcondition([&] (boost::optional<T const&> const& result) { + BOOST_CONTRACT_ASSERT(!full()); + BOOST_CONTRACT_ASSERT(*result == *old_item); + }) + ; + assert(false); + return *result; +} + +template<typename T> +void abstract_stack<T>::clear(boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(empty()); + }) + ; + assert(false); +} + +template<typename T> +class vstack + #define BASES private boost::contract::constructor_precondition< \ + vstack<T> >, public abstract_stack<T> + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + void invariant() const { + BOOST_CONTRACT_ASSERT(length() >= 0); + BOOST_CONTRACT_ASSERT(length() < capacity()); + } + + BOOST_CONTRACT_OVERRIDES(length, capacity, item, push, pop, clear) + +public: + explicit vstack(int count = 10) : + boost::contract::constructor_precondition<vstack>([&] { + BOOST_CONTRACT_ASSERT(count >= 0); + }), + vect_(count), // OK, executed after precondition so count >= 0. + len_(0) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(length() == 0); + BOOST_CONTRACT_ASSERT(capacity() == count); + }) + ; + } + + virtual ~vstack() { + boost::contract::check c = boost::contract::destructor(this); + } + + // Inherited from abstract_stack. + + virtual int length(boost::contract::virtual_* v = 0) const /* override */ { + int result; + boost::contract::check c = boost::contract::public_function< + override_length>(v, result, &vstack::length, this); + return result = len_; + } + + virtual int capacity(boost::contract::virtual_* v = 0) + const /* override */ { + int result; + boost::contract::check c = boost::contract::public_function< + override_capacity>(v, result, &vstack::capacity, this); + return result = vect_.size(); + } + + virtual T const& item(boost::contract::virtual_* v = 0) + const /* override */ { + boost::optional<T const&> result; + boost::contract::check c = boost::contract::public_function< + override_item>(v, result, &vstack::item, this); + return *(result = vect_[len_ - 1]); + } + + virtual void push(T const& value, boost::contract::virtual_* v = 0) + /* override */ { + boost::contract::check c = boost::contract::public_function< + override_push>(v, &vstack::push, this, value); + vect_[len_++] = value; + } + + virtual T const& pop(boost::contract::virtual_* v = 0) /* override */ { + boost::optional<T const&> result; + boost::contract::check c = boost::contract::public_function< + override_pop>(v, result, &vstack::pop, this); + return *(result = vect_[--len_]); + } + + virtual void clear(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_clear>(v, &vstack::clear, this); + len_ = 0; + } + +private: + vector<T> vect_; + int len_; +}; + +int main() { + vstack<int> s(3); + assert(s.capacity() == 3); + + s.push(123); + assert(s.length() == 1); + assert(s.pop() == 123); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/features/access.cpp b/src/boost/libs/contract/example/features/access.cpp new file mode 100644 index 000000000..075861728 --- /dev/null +++ b/src/boost/libs/contract/example/features/access.cpp @@ -0,0 +1,95 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <cassert> + +template<typename T> +class pushable { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(capacity() <= max_size()); + } + +public: + virtual void push_back(T const& value, boost::contract::virtual_* v = 0) + = 0; + +protected: + virtual unsigned capacity() const = 0; + virtual unsigned max_size() const = 0; +}; + +template<typename T> +void pushable<T>::push_back(T const& value, boost::contract::virtual_* v) { + boost::contract::old_ptr<unsigned> old_capacity = + BOOST_CONTRACT_OLDOF(v, capacity()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(capacity() < max_size()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + }) + ; + assert(false); +} + +//[access +template<typename T> +class vector + #define BASES public pushable<T> + : BASES +{ // Private section of the class. + friend class boost::contract::access; // Friend `access` class so... + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // ...private bases. + #undef BASES + + void invariant() const { // ...private invariants. + BOOST_CONTRACT_ASSERT(size() <= capacity()); + } + + BOOST_CONTRACT_OVERRIDE(push_back) // ...private overrides. + +public: // Public section of the class. + void push_back(T const& value, boost::contract::virtual_* v = 0) + /* override */ { + boost::contract::old_ptr<unsigned> old_size = + BOOST_CONTRACT_OLDOF(v, size()); + boost::contract::check c = boost::contract::public_function< + override_push_back>(v, &vector::push_back, this, value) + .precondition([&] { + BOOST_CONTRACT_ASSERT(size() < max_size()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + }) + ; + + vect_.push_back(value); + } + + /* ... */ +//] + + unsigned size() const { return vect_.size(); } + unsigned max_size() const { return vect_.max_size(); } + unsigned capacity() const { return vect_.capacity(); } + +private: // Another private section. + std::vector<T> vect_; +}; + +int main() { + vector<int> vect; + vect.push_back(123); + assert(vect.size() == 1); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/assertion_level.cpp b/src/boost/libs/contract/example/features/assertion_level.cpp new file mode 100644 index 000000000..c347b19c7 --- /dev/null +++ b/src/boost/libs/contract/example/features/assertion_level.cpp @@ -0,0 +1,135 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <algorithm> +#include <iostream> +#include <cassert> + +//[assertion_level_no_impl +// If valid iterator range (cannot implement in C++ but OK to use in AXIOM). +template<typename Iter> +bool valid(Iter first, Iter last); // Only declared, not actually defined. +//] + +//[assertion_level_class_begin +template<typename T> +class vector { +//] + +public: + typedef typename std::vector<T>::iterator iterator; + + // Could program class invariants and contracts for the following. + iterator begin() { return vect_.begin(); } + iterator end() { return vect_.end(); } + unsigned capacity() const { return vect_.capacity(); } + bool operator==(vector const& other) { return vect_ == other.vect_; } + +//[assertion_level_axiom +public: + iterator insert(iterator where, T const& value) { + iterator result; + boost::contract::old_ptr<unsigned> old_capacity = + BOOST_CONTRACT_OLDOF(capacity()); + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + if(capacity() > *old_capacity) { + BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end())); + } else { + BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end())); + } + }) + ; + + return result = vect_.insert(where, value); + } +//] + +//[assertion_level_audit_old +public: + void swap(vector& other) { + boost::contract::old_ptr<vector> old_me, old_other; + #ifdef BOOST_CONTRACT_AUDITS + old_me = BOOST_CONTRACT_OLDOF(*this); + old_other = BOOST_CONTRACT_OLDOF(other); + #endif // Else, skip old value copies... + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // ...and also skip related assertions. + BOOST_CONTRACT_ASSERT_AUDIT(*this == *old_other); + BOOST_CONTRACT_ASSERT_AUDIT(other == *old_me); + }) + ; + + vect_.swap(other.vect_); + } +//] + +//[assertion_level_class_end + /* ... */ + +private: + std::vector<T> vect_; +}; +//] + +//[assertion_level_audit +template<typename RandomIter, typename T> +RandomIter random_binary_search(RandomIter first, RandomIter last, + T const& value) { + RandomIter result; + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(first <= last); // Default, not expensive. + // Expensive O(n) assertion (use AXIOM if prohibitive instead). + BOOST_CONTRACT_ASSERT_AUDIT(std::is_sorted(first, last)); + }) + .postcondition([&] { + if(result != last) BOOST_CONTRACT_ASSERT(*result == value); + }) + ; + + /* ... */ +//] + + RandomIter begin = first, end = last; + while(begin < end) { + RandomIter middle = begin + ((end - begin) >> 1); + BOOST_CONTRACT_CHECK(*begin <= *middle || value < *middle || + *middle < value); + + if(value < *middle) end = middle; + else if(value > *middle) begin = middle + 1; + else return result = middle; + } + return result = last; +} + +int main() { + vector<char> v; + v.insert(v.begin() + 0, 'a'); + v.insert(v.begin() + 1, 'b'); + v.insert(v.begin() + 2, 'c'); + + vector<char>::iterator i = random_binary_search(v.begin(), v.end(), 'b'); + assert(i != v.end()); + assert(*i == 'b'); + + vector<char> w; + w.insert(w.begin() + 0, 'x'); + w.insert(w.begin() + 1, 'y'); + + w.swap(v); + assert(*(w.begin() + 0) == 'a'); + assert(*(w.begin() + 1) == 'b'); + assert(*(w.begin() + 2) == 'c'); + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/base_types.cpp b/src/boost/libs/contract/example/features/base_types.cpp new file mode 100644 index 000000000..56efcbfe0 --- /dev/null +++ b/src/boost/libs/contract/example/features/base_types.cpp @@ -0,0 +1,188 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <algorithm> +#include <cassert> + +template<typename T> +class pushable { +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(capacity() <= max_size()); + } + + virtual void push_back(T x, boost::contract::virtual_* v = 0) = 0; + +protected: + virtual unsigned capacity() const = 0; + virtual unsigned max_size() const = 0; +}; + +template<typename T> +void pushable<T>::push_back(T x, boost::contract::virtual_* v) { + boost::contract::old_ptr<unsigned> old_capacity = + BOOST_CONTRACT_OLDOF(v, capacity()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(capacity() < max_size()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + }) + ; + assert(false); // Shall never execute this body. +} + +struct has_size { virtual unsigned size() const = 0; }; +struct has_empty { virtual bool empty() const = 0; }; + +class unique_chars + : private boost::contract::constructor_precondition<unique_chars> +{ +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(size() >= 0); + } + + unique_chars(char from, char to) : + boost::contract::constructor_precondition<unique_chars>([&] { + BOOST_CONTRACT_ASSERT(from <= to); + }) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1)); + }) + ; + + for(char x = from; x <= to; ++x) vect_.push_back(x); + } + + virtual ~unique_chars() { + boost::contract::check c = boost::contract::destructor(this); + } + + unsigned size() const { + boost::contract::check c = boost::contract::public_function(this); + return vect_.size(); + } + + bool find(char x) const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + if(size() == 0) BOOST_CONTRACT_ASSERT(!result); + }) + ; + + return result = std::find(vect_.begin(), vect_.end(), x) != vect_.end(); + } + + virtual void push_back(char x, boost::contract::virtual_* v = 0) { + boost::contract::old_ptr<bool> old_find = + BOOST_CONTRACT_OLDOF(v, find(x)); + boost::contract::old_ptr<unsigned> old_size = + BOOST_CONTRACT_OLDOF(v, size()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!find(x)); + }) + .postcondition([&] { + if(!*old_find) { + BOOST_CONTRACT_ASSERT(find(x)); + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + } + }) + ; + + vect_.push_back(x); + } + +protected: + unique_chars() {} + + std::vector<char> const& vect() const { return vect_; } + +private: + std::vector<char> vect_; +}; + +//[base_types +class chars + #define BASES /* local macro (for convenience) */ \ + private boost::contract::constructor_precondition<chars>, \ + public unique_chars, \ + public virtual pushable<char>, \ + virtual protected has_size, \ + private has_empty + : BASES // Bases of this class. +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Bases typedef. + #undef BASES // Undefine local macro. + + /* ... */ +//] + + void invariant() const { + BOOST_CONTRACT_ASSERT(empty() == (size() == 0)); + } + + chars(char from, char to) : unique_chars(from, to) { + boost::contract::check c = boost::contract::constructor(this); + } + + chars(char const* const c_str) : + boost::contract::constructor_precondition<chars>([&] { + BOOST_CONTRACT_ASSERT(c_str[0] != '\0'); + }) + { + boost::contract::check c = boost::contract::constructor(this); + + for(unsigned i = 0; c_str[i] != '\0'; ++i) push_back(c_str[i]); + } + + void push_back(char x, boost::contract::virtual_* v = 0) /* override */ { + boost::contract::old_ptr<bool> old_find = + BOOST_CONTRACT_OLDOF(v, find(x)); + boost::contract::old_ptr<unsigned> old_size = + BOOST_CONTRACT_OLDOF(v, size()); + boost::contract::check c = boost::contract::public_function< + override_push_back>(v, &chars::push_back, this, x) + .precondition([&] { + BOOST_CONTRACT_ASSERT(find(x)); + }) + .postcondition([&] { + if(*old_find) BOOST_CONTRACT_ASSERT(size() == *old_size); + }) + ; + + if(!find(x)) unique_chars::push_back(x); + } + BOOST_CONTRACT_OVERRIDE(push_back); + + bool empty() const { + boost::contract::check c = boost::contract::public_function(this); + return size() == 0; + } + + unsigned size() const { return unique_chars::size(); } + +protected: + unsigned max_size() const { return vect().max_size(); } + unsigned capacity() const { return vect().capacity(); } +}; + +int main() { + chars s("abc"); + assert(s.find('a')); + assert(s.find('b')); + assert(!s.find('x')); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/base_types_no_macro.cpp b/src/boost/libs/contract/example/features/base_types_no_macro.cpp new file mode 100644 index 000000000..f9add687c --- /dev/null +++ b/src/boost/libs/contract/example/features/base_types_no_macro.cpp @@ -0,0 +1,188 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <algorithm> +#include <cassert> + +template<typename T> +class pushable { +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(capacity() <= max_size()); + } + + virtual void push_back(T x, boost::contract::virtual_* v = 0) = 0; + +protected: + virtual unsigned capacity() const = 0; + virtual unsigned max_size() const = 0; +}; + +template<typename T> +void pushable<T>::push_back(T x, boost::contract::virtual_* v) { + boost::contract::old_ptr<unsigned> old_capacity = + BOOST_CONTRACT_OLDOF(v, capacity()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(capacity() < max_size()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + }) + ; + assert(false); // Shall never execute this body. +} + +struct has_size { virtual unsigned size() const = 0; }; +struct has_empty { virtual bool empty() const = 0; }; + +class unique_chars + : private boost::contract::constructor_precondition<unique_chars> +{ +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(size() >= 0); + } + + unique_chars(char from, char to) : + boost::contract::constructor_precondition<unique_chars>([&] { + BOOST_CONTRACT_ASSERT(from <= to); + }) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1)); + }) + ; + + for(char x = from; x <= to; ++x) vect_.push_back(x); + } + + virtual ~unique_chars() { + boost::contract::check c = boost::contract::destructor(this); + } + + unsigned size() const { + boost::contract::check c = boost::contract::public_function(this); + return vect_.size(); + } + + bool find(char x) const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + if(size() == 0) BOOST_CONTRACT_ASSERT(!result); + }) + ; + + return result = std::find(vect_.begin(), vect_.end(), x) != vect_.end(); + } + + virtual void push_back(char x, boost::contract::virtual_* v = 0) { + boost::contract::old_ptr<bool> old_find = + BOOST_CONTRACT_OLDOF(v, find(x)); + boost::contract::old_ptr<unsigned> old_size = + BOOST_CONTRACT_OLDOF(v, size()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!find(x)); + }) + .postcondition([&] { + if(!*old_find) { + BOOST_CONTRACT_ASSERT(find(x)); + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + } + }) + ; + + vect_.push_back(x); + } + +protected: + unique_chars() {} + + std::vector<char> const& vect() const { return vect_; } + +private: + std::vector<char> vect_; +}; + +//[base_types_no_macro +#include <boost/mpl/vector.hpp> + +class chars : + private boost::contract::constructor_precondition<chars>, + public unique_chars, + public virtual pushable<char>, + virtual protected has_size, + private has_empty +{ +public: + // Program `base_types` without macros (list only public bases). + typedef boost::mpl::vector<unique_chars, pushable<char> > base_types; + + /* ... */ +//] + + void invariant() const { + BOOST_CONTRACT_ASSERT(empty() == (size() == 0)); + } + + chars(char from, char to) : unique_chars(from, to) { + boost::contract::check c = boost::contract::constructor(this); + } + + chars(char const* const c_str) : + boost::contract::constructor_precondition<chars>([&] { + BOOST_CONTRACT_ASSERT(c_str[0] != '\0'); + }) + { + boost::contract::check c = boost::contract::constructor(this); + + for(unsigned i = 0; c_str[i] != '\0'; ++i) push_back(c_str[i]); + } + + void push_back(char x, boost::contract::virtual_* v = 0) /* override */ { + boost::contract::old_ptr<bool> old_find = + BOOST_CONTRACT_OLDOF(v, find(x)); + boost::contract::old_ptr<unsigned> old_size = + BOOST_CONTRACT_OLDOF(v, size()); + boost::contract::check c = boost::contract::public_function< + override_push_back>(v, &chars::push_back, this, x) + .precondition([&] { + BOOST_CONTRACT_ASSERT(find(x)); + }) + .postcondition([&] { + if(*old_find) BOOST_CONTRACT_ASSERT(size() == *old_size); + }) + ; + + if(!find(x)) unique_chars::push_back(x); + } + BOOST_CONTRACT_OVERRIDE(push_back); + + bool empty() const { + boost::contract::check c = boost::contract::public_function(this); + return size() == 0; + } + + unsigned size() const { return unique_chars::size(); } + +protected: + unsigned max_size() const { return vect().max_size(); } + unsigned capacity() const { return vect().capacity(); } +}; + +int main() { + chars s("abc"); + assert(s.find('a')); + assert(s.find('b')); + assert(!s.find('x')); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/call_if_cxx14.cpp b/src/boost/libs/contract/example/features/call_if_cxx14.cpp new file mode 100644 index 000000000..bdf4f424a --- /dev/null +++ b/src/boost/libs/contract/example/features/call_if_cxx14.cpp @@ -0,0 +1,92 @@ + +// 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 + +#include <boost/contract/call_if.hpp> +#include <type_traits> +#include <iterator> +#include <functional> // std::bind for generic lambdas. +#include <vector> +#include <list> +#include <sstream> + +template<typename Iter> +struct is_random_access_iterator : std::is_same< + typename std::iterator_traits<Iter>::iterator_category, + std::random_access_iterator_tag +> {}; + +template<typename Iter> +struct is_bidirectional_iterator : std::is_same< + typename std::iterator_traits<Iter>::iterator_category, + std::bidirectional_iterator_tag +> {}; + +template<typename Iter> +struct is_input_iterator : std::is_same< + typename std::iterator_traits<Iter>::iterator_category, + std::input_iterator_tag +> {}; + +//[call_if_cxx14 +template<typename Iter, typename Dist> +void myadvance(Iter& i, Dist n) { + Iter* p = &i; // So captures change actual pointed iterator value. + boost::contract::call_if<is_random_access_iterator<Iter> >( + std::bind([] (auto p, auto n) { // C++14 generic lambda. + *p += n; + }, p, n) + ).template else_if<is_bidirectional_iterator<Iter> >( + std::bind([] (auto p, auto n) { + if(n >= 0) while(n--) ++*p; + else while(n++) --*p; + }, p, n) + ).template else_if<is_input_iterator<Iter> >( + std::bind([] (auto p, auto n) { + while(n--) ++*p; + }, p, n) + ).else_( + std::bind([] (auto false_) { + static_assert(false_, "requires at least input iterator"); + }, std::false_type()) // Use constexpr value. + ); +} +//] + +struct x {}; // Test not an iterator (static_assert failure in else_ above). + +namespace std { + template<> + struct iterator_traits<x> { + typedef void iterator_category; + }; +} + +int main() { + std::vector<char> v; + v.push_back('a'); + v.push_back('b'); + v.push_back('c'); + v.push_back('d'); + std::vector<char>::iterator r = v.begin(); // Random iterator. + myadvance(r, 1); + assert(*r == 'b'); + + std::list<char> l(v.begin(), v.end()); + std::list<char>::iterator b = l.begin(); // Bidirectional iterator. + myadvance(b, 2); + assert(*b == 'c'); + + std::istringstream s("a b c d"); + std::istream_iterator<char> i(s); + myadvance(i, 3); + assert(*i == 'd'); + + // x j; + // myadvance(j, 0); // Error (correctly because x not even input iter). + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/check.cpp b/src/boost/libs/contract/example/features/check.cpp new file mode 100644 index 000000000..36aa9da3a --- /dev/null +++ b/src/boost/libs/contract/example/features/check.cpp @@ -0,0 +1,41 @@ + +// 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 + +#include <boost/contract.hpp> + +int gcd(int const a, int const b) { + int result; + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(a > 0); + BOOST_CONTRACT_ASSERT(b > 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(result <= a); + BOOST_CONTRACT_ASSERT(result <= b); + }) + ; + + int x = a, y = b; + while(x != y) { + if(x > y) x = x - y; + else y = y - x; + } + return result = x; +} + +//[check +int main() { + // Implementation checks (via nullary functor). + boost::contract::check c = [] { + BOOST_CONTRACT_ASSERT(gcd(12, 28) == 4); + BOOST_CONTRACT_ASSERT(gcd(4, 14) == 2); + }; + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/features/check_macro.cpp b/src/boost/libs/contract/example/features/check_macro.cpp new file mode 100644 index 000000000..80d9c66c0 --- /dev/null +++ b/src/boost/libs/contract/example/features/check_macro.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 + +#include <boost/contract.hpp> + +int gcd(int const a, int const b) { + int result; + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(a > 0); + BOOST_CONTRACT_ASSERT(b > 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(result <= a); + BOOST_CONTRACT_ASSERT(result <= b); + }) + ; + + int x = a, y = b; + while(x != y) { + if(x > y) x = x - y; + else y = y - x; + } + return result = x; +} + +//[check_macro +int main() { + // Implementation checks (via macro, disable run-/compile-time overhead). + BOOST_CONTRACT_CHECK(gcd(12, 28) == 4); + BOOST_CONTRACT_CHECK(gcd(4, 14) == 2); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/features/code_block.cpp b/src/boost/libs/contract/example/features/code_block.cpp new file mode 100644 index 000000000..2ec434aa2 --- /dev/null +++ b/src/boost/libs/contract/example/features/code_block.cpp @@ -0,0 +1,43 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <algorithm> +#include <limits> + +int main() { + std::vector<int> v; + v.push_back(1); + v.push_back(2); + v.push_back(3); + int total = 10; + + //[code_block + /* ... */ + + // Contract for a code block. + { // Code block entry (check preconditions). + boost::contract::old_ptr<int> old_total = BOOST_CONTRACT_OLDOF(total); + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(v.size() == 3); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(total == *old_total + v[0] + v[1] + v[2]); + }) + ; + + total += v[0] + v[1] + v[2]; // Code block body. + } // Code block exit (check postconditions and exceptions guarantees). + + /* ... */ + //] + + assert(total == 16); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/condition_if.cpp b/src/boost/libs/contract/example/features/condition_if.cpp new file mode 100644 index 000000000..c8ecb964e --- /dev/null +++ b/src/boost/libs/contract/example/features/condition_if.cpp @@ -0,0 +1,58 @@ + +// 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 + +#include <boost/contract.hpp> +#include <boost/type_traits/has_equal_to.hpp> +#include <boost/bind.hpp> +#include <vector> +#include <functional> +#include <cassert> + +//[condition_if +template<typename T> +class vector { +public: + void push_back(T const& value) { + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Instead of `ASSERT(back() == value)` for T without `==`. + BOOST_CONTRACT_ASSERT( + boost::contract::condition_if<boost::has_equal_to<T> >( + boost::bind(std::equal_to<T>(), + boost::cref(back()), + boost::cref(value) + ) + ) + ); + }) + ; + + vect_.push_back(value); + } + + /* ... */ +//] + + T const& back() const { return vect_.back(); } + +private: + std::vector<T> vect_; +}; + +int main() { + vector<int> v; + v.push_back(1); // Type `int` has `==` so check postcondition. + assert(v.back() == 1); + + struct i { int value; } j; + j.value = 10; + vector<i> w; + w.push_back(j); // Type `i` has no `==` so skip postcondition. + assert(j.value == 10); + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/friend.cpp b/src/boost/libs/contract/example/features/friend.cpp new file mode 100644 index 000000000..215cfa6dd --- /dev/null +++ b/src/boost/libs/contract/example/features/friend.cpp @@ -0,0 +1,69 @@ + +// 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 + +#include <boost/contract.hpp> +#include <string> +#include <cassert> + +//[friend_byte +class buffer; + +class byte { + friend bool operator==(buffer const& left, byte const& right); + +private: + char value_; + + /* ... */ +//] + +public: + // Could program invariants and contracts for following too. + explicit byte(char value) : value_(value) {} + bool empty() const { return value_ == '\0'; } +}; + +//[friend_buffer +class buffer { + // Friend functions are not member functions... + friend bool operator==(buffer const& left, byte const& right) { + // ...so check contracts via `function` (which won't check invariants). + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(!left.empty()); + BOOST_CONTRACT_ASSERT(!right.empty()); + }) + ; + + for(char const* x = left.values_.c_str(); *x != '\0'; ++x) { + if(*x != right.value_) return false; + } + return true; + } + +private: + std::string values_; + + /* ... */ +//] + +public: + // Could program invariants and contracts for following too. + explicit buffer(std::string const& values) : values_(values) {} + bool empty() const { return values_ == ""; } +}; + +int main() { + buffer p("aaa"); + byte a('a'); + assert(p == a); + + buffer q("aba"); + assert(!(q == a)); // No operator!=. + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/friend_invariant.cpp b/src/boost/libs/contract/example/features/friend_invariant.cpp new file mode 100644 index 000000000..b9f69bbea --- /dev/null +++ b/src/boost/libs/contract/example/features/friend_invariant.cpp @@ -0,0 +1,59 @@ + +// 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 + +#include <boost/contract.hpp> +#include <cassert> + +//[friend_invariant +template<typename T> +class positive { +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(value() > 0); + } + + // Can be considered an extension of enclosing class' public interface... + friend void swap(positive& object, T& value) { + boost::contract::old_ptr<T> old_object_value = + BOOST_CONTRACT_OLDOF(object.value()); + boost::contract::old_ptr<T> old_value = BOOST_CONTRACT_OLDOF(value); + // ...so it can be made to check invariants via `public_function`. + boost::contract::check c = boost::contract::public_function(&object) + .precondition([&] { + BOOST_CONTRACT_ASSERT(value > 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(object.value() == *old_value); + BOOST_CONTRACT_ASSERT(value == *old_object_value); + }) + ; + + T saved = object.value_; + object.value_ = value; + value = saved; + } + +private: + T value_; + + /* ... */ +//] + +public: + // Could program contracts for following too. + explicit positive(T const& value) : value_(value) {} + T value() const { return value_; } +}; + +int main() { + positive<int> i(123); + int x = 456; + swap(i, x); + assert(i.value() == 456); + assert(x == 123); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/if_constexpr.cpp b/src/boost/libs/contract/example/features/if_constexpr.cpp new file mode 100644 index 000000000..f4561f149 --- /dev/null +++ b/src/boost/libs/contract/example/features/if_constexpr.cpp @@ -0,0 +1,113 @@ + +// Copyright (C) 2008-2019 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 + +#include <boost/contract.hpp> +#include <boost/type_traits/has_equal_to.hpp> +#include <utility> +#include <cassert> + +//[if_constexpr +template<typename T> +void swap(T& x, T& y) { + constexpr bool b = boost::contract::is_old_value_copyable<T>::value && + boost::has_equal_to<T>::value; + boost::contract::old_ptr<T> old_x, old_y; + if constexpr(b) { // Contract requires copyable T... + old_x = BOOST_CONTRACT_OLDOF(x); + old_y = BOOST_CONTRACT_OLDOF(y); + } + boost::contract::check c = boost::contract::function() + .postcondition([&] { + if constexpr(b) { // ... and T with `==`... + BOOST_CONTRACT_ASSERT(x == *old_y); + BOOST_CONTRACT_ASSERT(y == *old_x); + } + }) + ; + + T t = std::move(x); // ...but body only requires movable T. + x = std::move(y); + y = std::move(t); +} +//] + +struct i { // Non-copyable but has operator==. + explicit i(int n) : n_(n) {} + + i(i const&) = delete; // Non-copyable. + i& operator=(i const&) = delete; + + i(i const&& o) : n_(o.n_) {} + i& operator=(i const&& o) { n_ = o.n_; return *this; } + + friend bool operator==(i const& l, i const& r) { // Operator==. + return l.n_ == r.n_; + } + +private: + int n_; +}; + +struct j { // Copyable but no operator==. + explicit j(int n) : n_(n) {} + + j(j const& o) : n_(o.n_) {} // Copyable. + j& operator=(j const& o) { n_ = o.n_; return *this; } + + j(j const&& o) : n_(o.n_) {} + j& operator=(j const&& o) { n_ = o.n_; return *this; } + + // No operator==. + +private: + int n_; +}; + +struct k { // Non-copyable and no operator==. + explicit k(int n) : n_(n) {} + + k(k const&) = delete; // Non-copyable. + k& operator=(k const&) = delete; + + k(k const&& o) : n_(o.n_) {} + k& operator=(k const&& o) { n_ = o.n_; return *this; } + + // No operator==. + +private: + int n_; +}; + +int main() { + { // Copyable and operator== (so checks postconditions). + int x = 123, y = 456; + swap(x, y); + assert(x == 456); + assert(y == 123); + } + + { // Non-copyable (so does not check postconditions). + i x{123}, y{456}; + swap(x, y); + assert(x == i{456}); + assert(y == i{123}); + } + + { // No operator== (so does not check postconditions). + j x{123}, y{456}; + swap(x, y); + // Cannot assert x and y because no operator==. + } + + { // Non-copyable and no operator== (so does not check postconditions). + k x{123}, y{456}; + swap(x, y); + // Cannot assert x and y because no operator==. + } + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/ifdef.cpp b/src/boost/libs/contract/example/features/ifdef.cpp new file mode 100644 index 000000000..74e74ee90 --- /dev/null +++ b/src/boost/libs/contract/example/features/ifdef.cpp @@ -0,0 +1,213 @@ + +// 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 + +#include <vector> +#include <limits> +#include <cassert> + +//[ifdef_function +// Use #ifdef to completely disable contract code compilation. +#include <boost/contract/core/config.hpp> +#ifndef BOOST_CONTRACT_NO_ALL + #include <boost/contract.hpp> +#endif + +int inc(int& x) { + int result; + #ifndef BOOST_CONTRACT_NO_OLDS + boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); + #endif + #ifndef BOOST_CONTRACT_NO_FUNCTIONS + boost::contract::check c = boost::contract::function() + #ifndef BOOST_CONTRACT_NO_PRECONDITIONS + .precondition([&] { + BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); + }) + #endif + #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS + .postcondition([&] { + BOOST_CONTRACT_ASSERT(x == *old_x + 1); + BOOST_CONTRACT_ASSERT(result == *old_x); + }) + #endif + ; + #endif + + return result = x++; +} +//] + +template<typename T> +class pushable { + #ifndef BOOST_CONTRACT_NO_ALL + friend class boost::contract::access; + #endif + + #ifndef BOOST_CONTRACT_NO_INVARIANTS + void invariant() const { + BOOST_CONTRACT_ASSERT(capacity() <= max_size()); + } + #endif + +public: + virtual void push_back( + T const& x + #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS + , boost::contract::virtual_* v = 0 + #endif + ) = 0; + +protected: + virtual unsigned capacity() const = 0; + virtual unsigned max_size() const = 0; +}; + +template<typename T> +void pushable<T>::push_back( + T const& x + #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS + , boost::contract::virtual_* v + #endif +) { + #ifndef BOOST_CONTRACT_NO_OLDS + boost::contract::old_ptr<unsigned> old_capacity = + BOOST_CONTRACT_OLDOF(v, capacity()); + #endif + #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS + boost::contract::check c = boost::contract::public_function(v, this) + #ifndef BOOST_CONTRACT_NO_PRECONDITIONS + .precondition([&] { + BOOST_CONTRACT_ASSERT(capacity() < max_size()); + }) + #endif + #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS + .postcondition([&] { + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + }) + #endif + ; + #endif + assert(false); // Shall never execute this body. +} + +//[ifdef_class +class integers + #define BASES public pushable<int> + : + #ifndef BOOST_CONTRACT_NO_PRECONDITIONS + private boost::contract::constructor_precondition<integers>, BASES + #else + BASES + #endif +{ + #ifndef BOOST_CONTRACT_NO_ALL + friend class boost::contract::access; + #endif + + #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #endif + #undef BASES + + #ifndef BOOST_CONTRACT_NO_INVARIANTS + void invariant() const { + BOOST_CONTRACT_ASSERT(size() <= capacity()); + } + #endif + +public: + integers(int from, int to) : + #ifndef BOOST_CONTRACT_NO_PRECONDITIONS + boost::contract::constructor_precondition<integers>([&] { + BOOST_CONTRACT_ASSERT(from <= to); + }), + #endif + vect_(to - from + 1) + { + #ifndef BOOST_CONTRACT_NO_CONSTRUCTORS + boost::contract::check c = boost::contract::constructor(this) + #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS + .postcondition([&] { + BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1)); + }) + #endif + ; + #endif + + for(int x = from; x <= to; ++x) vect_.at(x - from) = x; + } + + virtual ~integers() { + #ifndef BOOST_CONTRACT_NO_DESTRUCTORS + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + #endif + } + + virtual void push_back( + int const& x + #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS + , boost::contract::virtual_* v = 0 + #endif + ) /* override */ { + #ifndef BOOST_CONTRACT_NO_OLDS + boost::contract::old_ptr<unsigned> old_size; + #endif + #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS + boost::contract::check c = boost::contract::public_function< + override_push_back>(v, &integers::push_back, this, x) + #ifndef BOOST_CONTRACT_NO_PRECONDITIONS + .precondition([&] { + BOOST_CONTRACT_ASSERT(size() < max_size()); + }) + #endif + #ifndef BOOST_CONTRACT_NO_OLDS + .old([&] { + old_size = BOOST_CONTRACT_OLDOF(v, size()); + }) + #endif + #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS + .postcondition([&] { + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + }) + #endif + #ifndef BOOST_CONTRACT_NO_EXCEPTS + .except([&] { + BOOST_CONTRACT_ASSERT(size() == *old_size); + }) + #endif + ; + #endif + + vect_.push_back(x); + } + +private: + #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS + BOOST_CONTRACT_OVERRIDE(push_back) + #endif + + /* ... */ +//] + +public: // Could program contracts for these too... + unsigned size() const { return vect_.size(); } + unsigned max_size() const { return vect_.max_size(); } + unsigned capacity() const { return vect_.capacity(); } + +private: + std::vector<int> vect_; +}; + +int main() { + integers i(1, 10); + int x = 123; + i.push_back(inc(x)); + assert(x == 124); + assert(i.size() == 11); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/ifdef_macro.cpp b/src/boost/libs/contract/example/features/ifdef_macro.cpp new file mode 100644 index 000000000..cc979bfd7 --- /dev/null +++ b/src/boost/libs/contract/example/features/ifdef_macro.cpp @@ -0,0 +1,150 @@ + +// 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 + +#include <vector> +#include <limits> +#include <cassert> + +//[ifdef_macro_function +// Use macro interface to completely disable contract code compilation. +#include <boost/contract_macro.hpp> + +int inc(int& x) { + int result; + BOOST_CONTRACT_OLD_PTR(int)(old_x, x); + BOOST_CONTRACT_FUNCTION() + BOOST_CONTRACT_PRECONDITION([&] { + BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); + }) + BOOST_CONTRACT_POSTCONDITION([&] { + BOOST_CONTRACT_ASSERT(x == *old_x + 1); + BOOST_CONTRACT_ASSERT(result == *old_x); + }) + ; + + return result = x++; +} +//] + +template<typename T> +class pushable { + friend class boost::contract::access; // Left in code (almost no overhead). + + BOOST_CONTRACT_INVARIANT({ + BOOST_CONTRACT_ASSERT(capacity() <= max_size()); + }) + +public: + virtual void push_back( + T const& x, + boost::contract::virtual_* v = 0 // Left in code (almost no overhead). + ) = 0; + +protected: + virtual unsigned capacity() const = 0; + virtual unsigned max_size() const = 0; +}; + +template<typename T> +void pushable<T>::push_back(T const& x, boost::contract::virtual_* v) { + BOOST_CONTRACT_OLD_PTR(unsigned)(v, old_capacity, capacity()); + BOOST_CONTRACT_PUBLIC_FUNCTION(v, this) + BOOST_CONTRACT_PRECONDITION([&] { + BOOST_CONTRACT_ASSERT(capacity() < max_size()); + }) + BOOST_CONTRACT_POSTCONDITION([&] { + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + }) + ; + assert(false); // Shall never execute this body. +} + +//[ifdef_macro_class +class integers + #define BASES public pushable<int> + : + // Left in code (almost no overhead). + private boost::contract::constructor_precondition<integers>, + BASES +{ + // Followings left in code (almost no overhead). + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + BOOST_CONTRACT_INVARIANT({ + BOOST_CONTRACT_ASSERT(size() <= capacity()); + }) + +public: + integers(int from, int to) : + BOOST_CONTRACT_CONSTRUCTOR_PRECONDITION(integers)([&] { + BOOST_CONTRACT_ASSERT(from <= to); + }), + vect_(to - from + 1) + { + BOOST_CONTRACT_CONSTRUCTOR(this) + BOOST_CONTRACT_POSTCONDITION([&] { + BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1)); + }) + ; + + for(int x = from; x <= to; ++x) vect_.at(x - from) = x; + } + + virtual ~integers() { + BOOST_CONTRACT_DESTRUCTOR(this); // Check invariants. + } + + virtual void push_back( + int const& x, + boost::contract::virtual_* v = 0 // Left in code (almost no overhead). + ) /* override */ { + BOOST_CONTRACT_OLD_PTR(unsigned)(old_size); + BOOST_CONTRACT_PUBLIC_FUNCTION_OVERRIDE(override_push_back)( + v, &integers::push_back, this, x) + BOOST_CONTRACT_PRECONDITION([&] { + BOOST_CONTRACT_ASSERT(size() < max_size()); + }) + BOOST_CONTRACT_OLD([&] { + old_size = BOOST_CONTRACT_OLDOF(v, size()); + }) + BOOST_CONTRACT_POSTCONDITION([&] { + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + }) + BOOST_CONTRACT_EXCEPT([&] { + BOOST_CONTRACT_ASSERT(size() == *old_size); + }) + ; + + vect_.push_back(x); + } + +private: + BOOST_CONTRACT_OVERRIDE(push_back) // Left in code (almost no overhead). + + /* ... */ +//] + +public: // Could program contracts for these too... + unsigned size() const { return vect_.size(); } + unsigned max_size() const { return vect_.max_size(); } + unsigned capacity() const { return vect_.capacity(); } + +private: + std::vector<int> vect_; +}; + +int main() { + integers i(1, 10); + int x = 123; + i.push_back(inc(x)); + assert(x == 124); + assert(i.size() == 11); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/introduction.cpp b/src/boost/libs/contract/example/features/introduction.cpp new file mode 100644 index 000000000..25baf10fe --- /dev/null +++ b/src/boost/libs/contract/example/features/introduction.cpp @@ -0,0 +1,34 @@ + +// 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 + +#include <limits> +#include <cassert> + +//[introduction +#include <boost/contract.hpp> + +void inc(int& x) { + boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); // Old value. + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); // Line 17. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(x == *old_x + 1); // Line 20. + }) + ; + + ++x; // Function body. +} +//] + +int main() { + int x = 10; + inc(x); + assert(x == 11); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/introduction_comments.cpp b/src/boost/libs/contract/example/features/introduction_comments.cpp new file mode 100644 index 000000000..3eba12f84 --- /dev/null +++ b/src/boost/libs/contract/example/features/introduction_comments.cpp @@ -0,0 +1,24 @@ + +// 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 + +#include <cassert> + +//[introduction_comments +void inc(int& x) + // Precondition: x < std::numeric_limit<int>::max() + // Postcondition: x == oldof(x) + 1 +{ + ++x; // Function body. +} +//] + +int main() { + int x = 10; + inc(x); + assert(x == 11); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/introduction_public.cpp b/src/boost/libs/contract/example/features/introduction_public.cpp new file mode 100644 index 000000000..2206bcab9 --- /dev/null +++ b/src/boost/libs/contract/example/features/introduction_public.cpp @@ -0,0 +1,89 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <cassert> + +template<typename T> +class pushable { // Somewhat arbitrary base (used just to show subcontracting). +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(capacity() <= max_size()); + } + + virtual void push_back(T const& value, + boost::contract::virtual_* v = 0) = 0; // Pure virtual function. + +protected: + virtual unsigned capacity() const = 0; + virtual unsigned max_size() const = 0; +}; + +template<typename T> // Contract for pure virtual function. +void pushable<T>::push_back(T const& value, boost::contract::virtual_* v) { + boost::contract::old_ptr<unsigned> old_capacity = + BOOST_CONTRACT_OLDOF(v, capacity()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(capacity() < max_size()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + }) + ; + assert(false); // Shall never execute this body. +} + +//[introduction_public +template<typename T> +class vector + #define BASES public pushable<T> + : BASES +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // For subcontracting. + #undef BASES + + void invariant() const { // Checked in AND with base class invariants. + BOOST_CONTRACT_ASSERT(size() <= capacity()); + } + + virtual void push_back(T const& value, + boost::contract::virtual_* v = 0) /* override */ { // For virtuals. + boost::contract::old_ptr<unsigned> old_size = + BOOST_CONTRACT_OLDOF(v, size()); // Old values for virtuals. + boost::contract::check c = boost::contract::public_function< // For overrides. + override_push_back>(v, &vector::push_back, this, value) + .precondition([&] { // Checked in OR with base preconditions. + BOOST_CONTRACT_ASSERT(size() < max_size()); + }) + .postcondition([&] { // Checked in AND with base postconditions. + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + }) + ; + + vect_.push_back(value); + } + BOOST_CONTRACT_OVERRIDE(push_back) // Define `override_push_back` above. + + // Could program contracts for those as well. + unsigned size() const { return vect_.size(); } + unsigned max_size() const { return vect_.max_size(); } + unsigned capacity() const { return vect_.capacity(); } + +private: + std::vector<T> vect_; +}; +//] + +int main() { + vector<int> vect; + vect.push_back(123); + assert(vect.size() == 1); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/lambda.cpp b/src/boost/libs/contract/example/features/lambda.cpp new file mode 100644 index 000000000..6eb999801 --- /dev/null +++ b/src/boost/libs/contract/example/features/lambda.cpp @@ -0,0 +1,43 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <algorithm> +#include <limits> + +int main() { + std::vector<int> v; + v.push_back(1); + v.push_back(2); + v.push_back(3); + + //[lambda + int total = 0; + std::for_each(v.cbegin(), v.cend(), + // Contract for a lambda function. + [&total] (int const x) { + boost::contract::old_ptr<int> old_total = + BOOST_CONTRACT_OLDOF(total); + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT( + total < std::numeric_limits<int>::max() - x); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(total == *old_total + x); + }) + ; + + total += x; // Lambda function body. + } + ); + //] + + assert(total == 6); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/loop.cpp b/src/boost/libs/contract/example/features/loop.cpp new file mode 100644 index 000000000..1d8acdd71 --- /dev/null +++ b/src/boost/libs/contract/example/features/loop.cpp @@ -0,0 +1,40 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <algorithm> +#include <limits> + +int main() { + std::vector<int> v; + v.push_back(1); + v.push_back(2); + v.push_back(3); + + //[loop + int total = 0; + // Contract for a for-loop (same for while- and all other loops). + for(std::vector<int>::const_iterator i = v.begin(); i != v.end(); ++i) { + boost::contract::old_ptr<int> old_total = BOOST_CONTRACT_OLDOF(total); + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT( + total < std::numeric_limits<int>::max() - *i); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(total == *old_total + *i); + }) + ; + + total += *i; // For-loop body. + } + //] + + assert(total == 6); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/move.cpp b/src/boost/libs/contract/example/features/move.cpp new file mode 100644 index 000000000..de54d16a0 --- /dev/null +++ b/src/boost/libs/contract/example/features/move.cpp @@ -0,0 +1,201 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <utility> +#include <cassert> + +//[move +class circular_buffer : + private boost::contract::constructor_precondition<circular_buffer> { +public: + void invariant() const { + if(!moved()) { // Do not check (some) invariants for moved-from objects. + BOOST_CONTRACT_ASSERT(index() < size()); + } + // More invariants here that hold also for moved-from objects (e.g., + // all assertions necessary to successfully destroy moved-from objects). + } + + // Move constructor. + circular_buffer(circular_buffer&& other) : + boost::contract::constructor_precondition<circular_buffer>([&] { + BOOST_CONTRACT_ASSERT(!other.moved()); + }) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!moved()); + BOOST_CONTRACT_ASSERT(other.moved()); + }) + ; + + move(std::forward<circular_buffer>(other)); + } + + // Move assignment. + circular_buffer& operator=(circular_buffer&& other) { + // Moved-from can be (move) assigned (so no pre `!moved()` here). + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!other.moved()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!moved()); + BOOST_CONTRACT_ASSERT(other.moved()); + }) + ; + + return move(std::forward<circular_buffer>(other)); + } + + ~circular_buffer() { + // Moved-from can always be destroyed (in fact no preconditions). + boost::contract::check c = boost::contract::destructor(this); + } + + bool moved() const { + boost::contract::check c = boost::contract::public_function(this); + return moved_; + } + +private: + bool moved_; + + /* ... */ +//] + +public: + explicit circular_buffer(std::vector<char> const& data, + unsigned start = 0) : + boost::contract::constructor_precondition<circular_buffer>([&] { + BOOST_CONTRACT_ASSERT(start < data.size()); + }), + moved_(false), + data_(data), + index_(start) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!moved()); + }) + ; + } + + // Copy constructor. + circular_buffer(circular_buffer const& other) : + boost::contract::constructor_precondition<circular_buffer>([&] { + BOOST_CONTRACT_ASSERT(!other.moved()); + }) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!moved()); + }) + ; + + copy(other); + } + + // Copy assignment. + circular_buffer& operator=(circular_buffer const& other) { + // Moved-from can be (copy) assigned (so no pre `!moved()` here). + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!other.moved()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!moved()); + }) + ; + + return copy(other); + } + + char read() { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!moved()); + }) + ; + + unsigned i = index_++; + if(index_ == data_.size()) index_ = 0; // Circular. + return data_.at(i); + } + +private: + circular_buffer& copy(circular_buffer const& other) { + data_ = other.data_; + index_ = other.index_; + moved_ = false; + return *this; + } + + circular_buffer& move(circular_buffer&& other) { + data_ = std::move(other.data_); + index_ = std::move(other.index_); + moved_ = false; + other.moved_ = true; // Mark moved-from object. + return *this; + } + + std::vector<char> data_; + unsigned index_; + +public: + unsigned index() const { + boost::contract::check c = boost::contract::public_function(this); + return index_; + } + + unsigned size() const { + boost::contract::check c = boost::contract::public_function(this); + return data_.size(); + } +}; + +int main() { + struct err {}; + boost::contract::set_precondition_failure( + [] (boost::contract::from) { throw err(); }); + + { + circular_buffer x({'a', 'b', 'c', 'd'}, 2); + assert(x.read() == 'c'); + + circular_buffer y1 = x; // Copy constructor. + assert(y1.read() == 'd'); + assert(x.read() == 'd'); + + circular_buffer y2({'h'}); + y2 = x; // Copy assignment. + assert(y2.read() == 'a'); + assert(x.read() == 'a'); + + circular_buffer z1 = std::move(x); // Move constructor. + assert(z1.read() == 'b'); + // Calling `x.read()` would fail `!moved()` precondition. + + x = y1; // Moved-from `x` can be copy assigned. + assert(x.read() == 'a'); + assert(y1.read() == 'a'); + + circular_buffer z2({'k'}); + z2 = std::move(x); // Move assignment. + assert(z2.read() == 'b'); + // Calling `x.read()` would fail `!moved()` precondition. + + x = std::move(y2); // Moved-from `x` can be move assigned. + assert(x.read() == 'b'); + // Calling `y2.read()` would fail `!moved()` precondition. + + } // Moved-from `y2` can be destroyed. + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/named_override.cpp b/src/boost/libs/contract/example/features/named_override.cpp new file mode 100644 index 000000000..9afc5f60a --- /dev/null +++ b/src/boost/libs/contract/example/features/named_override.cpp @@ -0,0 +1,104 @@ + +// 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 + +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <cassert> + +//[named_override_pure_virtual_assert_false +template<typename T> +class generic_unary_pack { +public: + virtual void _1(T const& value, boost::contract::virtual_* v = 0) = 0; + virtual T _1(boost::contract::virtual_* v = 0) const = 0; +}; + +template<typename T> +void generic_unary_pack<T>::_1(T const& value, boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(false); // Defer preconditions to overrides. + }) + ; + assert(false); +} + +/* ... */ +//] + +template<typename T> +T generic_unary_pack<T>::_1(boost::contract::virtual_* v) const { + boost::optional<T> result; // Do not assume T has default constructor. + boost::contract::check c = boost::contract::public_function(v, result, this) + .postcondition([&] (boost::optional<T const&> const& result) { + BOOST_CONTRACT_ASSERT(*result == _1()); + }) + ; + + assert(false); + return *result; +} + +//[named_override +template<typename T> +class positive_unary_pack + #define BASES public generic_unary_pack<T> + : BASES +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + // BOOST_CONTRACT_OVERRIDE(_1) would generate reserved name `override__1`. + BOOST_CONTRACT_NAMED_OVERRIDE(override1, _1) // Generate `override1`. + + virtual void _1(T const& value, boost::contract::virtual_* v = 0) + /* override */ { + // Use `override1` generated by BOOST_CONTRACT_NAMED_OVERRIDE above. + boost::contract::check c = boost::contract::public_function<override1>( + v, + static_cast<void (positive_unary_pack::*)(T const&, + boost::contract::virtual_*)>(&positive_unary_pack::_1), + this, + value + ) + .precondition([&] { + BOOST_CONTRACT_ASSERT(value > 0); + }) + ; + value1_ = value; + } + + /* ... */ +//] + + virtual T _1(boost::contract::virtual_* v = 0) const /* override */ { + T result; // Class default constructor already used T's default ctor. + boost::contract::check c = boost::contract::public_function<override1>( + v, + result, + static_cast<T (positive_unary_pack::*)(boost::contract::virtual_*) + const>(&positive_unary_pack::_1), + this + ) + .postcondition([&] (T const& result) { + BOOST_CONTRACT_ASSERT(result > 0); + }) + ; + return result = value1_; + } + +private: + T value1_; +}; + +int main() { + positive_unary_pack<int> u; + u._1(123); + assert(u._1() == 123); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/no_lambdas.cpp b/src/boost/libs/contract/example/features/no_lambdas.cpp new file mode 100644 index 000000000..783adce59 --- /dev/null +++ b/src/boost/libs/contract/example/features/no_lambdas.cpp @@ -0,0 +1,92 @@ + +// 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 + +#include "no_lambdas.hpp" +#include <boost/bind.hpp> +#include <cassert> + +//[no_lambdas_cpp +iarray::iarray(unsigned max, unsigned count) : + boost::contract::constructor_precondition<iarray>(boost::bind( + &iarray::constructor_precondition, max, count)), + values_(new int[max]), // Member initializations can be here. + capacity_(max) +{ + boost::contract::old_ptr<int> old_instances; + boost::contract::check c = boost::contract::constructor(this) + .old(boost::bind(&iarray::constructor_old, boost::ref(old_instances))) + .postcondition(boost::bind( + &iarray::constructor_postcondition, + this, + boost::cref(max), + boost::cref(count), + boost::cref(old_instances) + )) + ; + + for(unsigned i = 0; i < count; ++i) values_[i] = int(); + size_ = count; + ++instances_; +} + +iarray::~iarray() { + boost::contract::old_ptr<int> old_instances; + boost::contract::check c = boost::contract::destructor(this) + .old(boost::bind(&iarray::destructor_old, this, + boost::ref(old_instances))) + .postcondition(boost::bind(&iarray::destructor_postcondition, + boost::cref(old_instances))) + ; + + delete[] values_; + --instances_; +} + +void iarray::push_back(int value, boost::contract::virtual_* v) { + boost::contract::old_ptr<unsigned> old_size; + boost::contract::check c = boost::contract::public_function(v, this) + .precondition(boost::bind(&iarray::push_back_precondition, this)) + .old(boost::bind(&iarray::push_back_old, this, boost::cref(v), + boost::ref(old_size))) + .postcondition(boost::bind(&iarray::push_back_postcondition, this, + boost::cref(old_size))) + ; + + values_[size_++] = value; +} + +unsigned iarray::capacity() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return capacity_; +} + +unsigned iarray::size() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return size_; +} + +int iarray::instances() { + // Check static invariants. + boost::contract::check c = boost::contract::public_function<iarray>(); + return instances_; +} + +int iarray::instances_ = 0; +//] + +int main() { + iarray a(3, 2); + assert(a.capacity() == 3); + assert(a.size() == 2); + + a.push_back(-123); + assert(a.size() == 3); + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/no_lambdas.hpp b/src/boost/libs/contract/example/features/no_lambdas.hpp new file mode 100644 index 000000000..5f0dbe725 --- /dev/null +++ b/src/boost/libs/contract/example/features/no_lambdas.hpp @@ -0,0 +1,77 @@ + +#ifndef NO_LAMBDAS_HPP_ +#define NO_LAMBDAS_HPP_ + +// 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 + +#include <boost/contract.hpp> + +//[no_lambdas_hpp +class iarray : + private boost::contract::constructor_precondition<iarray> { +public: + static void static_invariant() { + BOOST_CONTRACT_ASSERT(instances() >= 0); + } + + void invariant() const { + BOOST_CONTRACT_ASSERT(size() <= capacity()); + } + + explicit iarray(unsigned max, unsigned count = 0); + static void constructor_precondition(unsigned const max, + unsigned const count) { + BOOST_CONTRACT_ASSERT(count <= max); + } + static void constructor_old(boost::contract::old_ptr<int>& + old_instances) { + old_instances = BOOST_CONTRACT_OLDOF(instances()); + } + void constructor_postcondition(unsigned const max, unsigned const count, + boost::contract::old_ptr<int> const old_instances) const { + BOOST_CONTRACT_ASSERT(capacity() == max); + BOOST_CONTRACT_ASSERT(size() == count); + BOOST_CONTRACT_ASSERT(instances() == *old_instances + 1); + } + + virtual ~iarray(); + void destructor_old(boost::contract::old_ptr<int>& old_instances) + const { + old_instances = BOOST_CONTRACT_OLDOF(instances()); + } + static void destructor_postcondition(boost::contract::old_ptr<int> const + old_instances) { + BOOST_CONTRACT_ASSERT(instances() == *old_instances - 1); + } + + virtual void push_back(int value, boost::contract::virtual_* v = 0); + void push_back_precondition() const { + BOOST_CONTRACT_ASSERT(size() < capacity()); + } + void push_back_old(boost::contract::virtual_* v, + boost::contract::old_ptr<unsigned>& old_size) const { + old_size = BOOST_CONTRACT_OLDOF(v, size()); + } + void push_back_postcondition( + boost::contract::old_ptr<unsigned> const old_size) const { + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + } + + unsigned capacity() const; + unsigned size() const; + + static int instances(); + +private: + int* values_; + unsigned capacity_; + unsigned size_; + static int instances_; +}; +//] + +#endif // #include guard + diff --git a/src/boost/libs/contract/example/features/no_lambdas_local_func.cpp b/src/boost/libs/contract/example/features/no_lambdas_local_func.cpp new file mode 100644 index 000000000..801e1639a --- /dev/null +++ b/src/boost/libs/contract/example/features/no_lambdas_local_func.cpp @@ -0,0 +1,119 @@ + +// 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 + +#include <boost/contract.hpp> +#include <boost/local_function.hpp> +#include <boost/bind.hpp> +#include <cassert> + +class iarray : + private boost::contract::constructor_precondition<iarray> { +public: + static void static_invariant() { + BOOST_CONTRACT_ASSERT(instances() >= 0); + } + + void invariant() const { + BOOST_CONTRACT_ASSERT(size() <= capacity()); + } + + static void constructor_pre(unsigned const max, unsigned const count) { + BOOST_CONTRACT_ASSERT(count <= max); + } + explicit iarray(unsigned max, unsigned count = 0) : + boost::contract::constructor_precondition<iarray>(boost::bind( + &iarray::constructor_pre, max, count)), + values_(new int[max]), + capacity_(max) + { + boost::contract::old_ptr<int> old_instances; + void BOOST_LOCAL_FUNCTION(bind& old_instances) { + old_instances = BOOST_CONTRACT_OLDOF(iarray::instances()); + } BOOST_LOCAL_FUNCTION_NAME(old) + void BOOST_LOCAL_FUNCTION(const bind this_, const bind& count, + const bind& old_instances) { + BOOST_CONTRACT_ASSERT(this_->size() == count); + BOOST_CONTRACT_ASSERT(this_->instances() == *old_instances + 1); + } BOOST_LOCAL_FUNCTION_NAME(post) + boost::contract::check c = boost::contract::constructor(this) + .old(old).postcondition(post); + + for(unsigned i = 0; i < count; ++i) values_[i] = int(); + size_ = count; + ++instances_; + } + + virtual ~iarray() { + boost::contract::old_ptr<int> old_instances; + void BOOST_LOCAL_FUNCTION(const bind this_, bind& old_instances) { + old_instances = BOOST_CONTRACT_OLDOF(this_->instances()); + } BOOST_LOCAL_FUNCTION_NAME(old) + void BOOST_LOCAL_FUNCTION(const bind& old_instances) { + BOOST_CONTRACT_ASSERT(iarray::instances() == *old_instances - 1); + } BOOST_LOCAL_FUNCTION_NAME(post) + boost::contract::check c = boost::contract::destructor(this) + .old(old).postcondition(post); + + delete[] values_; + --instances_; + } + + virtual void push_back(int value, boost::contract::virtual_* v = 0) { + boost::contract::old_ptr<unsigned> old_size; + void BOOST_LOCAL_FUNCTION(const bind this_) { + BOOST_CONTRACT_ASSERT(this_->size() < this_->capacity()); + } BOOST_LOCAL_FUNCTION_NAME(pre) + void BOOST_LOCAL_FUNCTION(const bind v, const bind this_, + bind& old_size) { + old_size = BOOST_CONTRACT_OLDOF(v, this_->size()); + } BOOST_LOCAL_FUNCTION_NAME(old) + void BOOST_LOCAL_FUNCTION(const bind this_, const bind& old_size) { + BOOST_CONTRACT_ASSERT(this_->size() == *old_size + 1); + } BOOST_LOCAL_FUNCTION_NAME(post) + boost::contract::check c = boost::contract::public_function(v, this) + .precondition(pre).old(old).postcondition(post); + + values_[size_++] = value; + } + + unsigned capacity() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return capacity_; + } + + unsigned size() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return size_; + } + + static int instances() { + // Check static invariants. + boost::contract::check c = boost::contract::public_function<iarray>(); + return instances_; + } + +private: + int* values_; + unsigned capacity_; + unsigned size_; + static int instances_; +}; + +int iarray::instances_ = 0; + +int main() { + iarray a(3, 2); + assert(a.capacity() == 3); + assert(a.size() == 2); + + a.push_back('x'); + assert(a.size() == 3); + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/non_member.cpp b/src/boost/libs/contract/example/features/non_member.cpp new file mode 100644 index 000000000..122241549 --- /dev/null +++ b/src/boost/libs/contract/example/features/non_member.cpp @@ -0,0 +1,40 @@ + +// 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 + +#include <limits> +#include <cassert> + +//[non_member +#include <boost/contract.hpp> + +// Contract for a non-member function. +int inc(int& x) { + int result; + boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(x == *old_x + 1); + BOOST_CONTRACT_ASSERT(result == *old_x); + }) + .except([&] { + BOOST_CONTRACT_ASSERT(x == *old_x); + }) + ; + + return result = x++; // Function body. +} +//] + +int main() { + int x = std::numeric_limits<int>::max() - 1; + assert(inc(x) == std::numeric_limits<int>::max() - 1); + assert(x == std::numeric_limits<int>::max()); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/old.cpp b/src/boost/libs/contract/example/features/old.cpp new file mode 100644 index 000000000..bdf8b8c6e --- /dev/null +++ b/src/boost/libs/contract/example/features/old.cpp @@ -0,0 +1,41 @@ + +// 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 + +#include <boost/contract.hpp> +#include <string> +#include <cassert> + +//[old +char replace(std::string& s, unsigned index, char x) { + char result; + boost::contract::old_ptr<char> old_char; // Null, old value copied later... + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(index < s.size()); + }) + .old([&] { // ...after preconditions (and invariants) checked. + old_char = BOOST_CONTRACT_OLDOF(s[index]); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(s[index] == x); + BOOST_CONTRACT_ASSERT(result == *old_char); + }) + ; + + result = s[index]; + s[index] = x; + return result; +} +//] + +int main() { + std::string s = "abc"; + char r = replace(s, 1, '_'); + assert(s == "a_c"); + assert(r == 'b'); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/old_if_copyable.cpp b/src/boost/libs/contract/example/features/old_if_copyable.cpp new file mode 100644 index 000000000..8cf1acc7b --- /dev/null +++ b/src/boost/libs/contract/example/features/old_if_copyable.cpp @@ -0,0 +1,133 @@ + +// 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 + +#include <boost/contract.hpp> +#include <boost/type_traits.hpp> +#include <boost/noncopyable.hpp> +#include <cassert> + +//[old_if_copyable_offset +template<typename T> // T might or might not be copyable. +void offset(T& x, int count) { + // No compiler error if T has no copy constructor... + boost::contract::old_ptr_if_copyable<T> old_x = BOOST_CONTRACT_OLDOF(x); + boost::contract::check c = boost::contract::function() + .postcondition([&] { + // ...but old value null if T has no copy constructor. + if(old_x) BOOST_CONTRACT_ASSERT(x == *old_x + count); + }) + ; + + x += count; +} +//] + +//[old_if_copyable_w_decl +// Copyable type but... +class w { +public: + w(w const&) { /* Some very expensive copy operation here... */ } + + /* ... */ +//] + w() : num_(0) {} + int operator+(int i) const { return num_ + i; } + w& operator+=(int i) { num_ += i; return *this; } + bool operator==(int i) const { return long(num_) == i; } +private: + unsigned long num_; +}; + +//[old_if_copyable_w_spec +// ...never copy old values for type `w` (because its copy is too expensive). +namespace boost { namespace contract { + template<> + struct is_old_value_copyable<w> : boost::false_type {}; +} } +//] + +//[old_if_copyable_p_decl +// Non-copyable type but... +class p : private boost::noncopyable { + int* num_; + + friend struct boost::contract::old_value_copy<p>; + + /* ... */ +//] +public: + p() : num_(new int(0)) {} + ~p() { delete num_; } + int operator+(int i) const { return *num_ + i; } + p& operator+=(int i) { *num_ += i; return *this; } + bool operator==(int i) const { return *num_ == i; } +}; + +//[old_if_copyable_p_spec +// ...still copy old values for type `p` (using a deep copy). +namespace boost { namespace contract { + template<> + struct old_value_copy<p> { + explicit old_value_copy(p const& old) { + *old_.num_ = *old.num_; // Deep copy pointed value. + } + + p const& old() const { return old_; } + + private: + p old_; + }; + + template<> + struct is_old_value_copyable<p> : boost::true_type {}; +} } +//] + +//[old_if_copyable_n_decl +class n { // Do not want to use boost::noncopyable but... + int num_; + +private: + n(n const&); // ...unimplemented private copy constructor (so non-copyable). + + /* ... */ +//] + +public: + n() : num_(0) {} + int operator+(int i) const { return num_ + i; } + n& operator+=(int i) { num_ += i; return *this; } + bool operator==(int i) const { return num_ == i; } +}; + +//[old_if_copyable_n_spec +// Specialize `boost::is_copy_constructible` (no need for this on C++11). +namespace boost { namespace contract { + template<> + struct is_old_value_copyable<n> : boost::false_type {}; +} } +//] + +int main() { + int i = 0; // Copy constructor, copy and check old values. + offset(i, 3); + assert(i == 3); + + w j; // Expensive copy constructor, so never copy or check old values. + offset(j, 3); + assert(j == 3); + + p k; // No copy constructor, but still copy and check old values. + offset(k, 3); + assert(k == 3); + + n h; // No copy constructor, no compiler error but no old value checks. + offset(h, 3); + assert(h == 3); + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/old_no_macro.cpp b/src/boost/libs/contract/example/features/old_no_macro.cpp new file mode 100644 index 000000000..29c06a681 --- /dev/null +++ b/src/boost/libs/contract/example/features/old_no_macro.cpp @@ -0,0 +1,46 @@ + +// 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 + +#include <boost/contract.hpp> +#include <cassert> +#include <vector> + +//[old_no_macro +template<typename T> +class vector { +public: + virtual void push_back(T const& value, boost::contract::virtual_* v = 0) { + // Program old value instead of using `OLD(size())` macro. + boost::contract::old_ptr<unsigned> old_size = + boost::contract::make_old(v, boost::contract::copy_old(v) ? + size() : boost::contract::null_old()) + ; + + boost::contract::check c = boost::contract::public_function(v, this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + }) + ; + + vect_.push_back(value); + } + + /* ... */ +//] + + unsigned size() const { return vect_.size(); } + +private: + std::vector<T> vect_; +}; + +int main() { + vector<int> vect; + vect.push_back(123); + assert(vect.size() == 1); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/optional_result.cpp b/src/boost/libs/contract/example/features/optional_result.cpp new file mode 100644 index 000000000..330c780de --- /dev/null +++ b/src/boost/libs/contract/example/features/optional_result.cpp @@ -0,0 +1,41 @@ + +// 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 + +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <vector> +#include <cassert> + +//[optional_result +template<unsigned Index, typename T> +T& get(std::vector<T>& vect) { + boost::optional<T&> result; // Result not initialized here... + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(Index < vect.size()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(*result == vect[Index]); + }) + ; + + // Function body (executed after preconditions checked). + return *(result = vect[Index]); // ...result initialized here instead. +} +//] + +int main() { + std::vector<int> v; + v.push_back(123); + v.push_back(456); + v.push_back(789); + int& x = get<1>(v); + assert(x == 456); + x = -456; + assert(v[1] == -456); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/optional_result_virtual.cpp b/src/boost/libs/contract/example/features/optional_result_virtual.cpp new file mode 100644 index 000000000..724a18493 --- /dev/null +++ b/src/boost/libs/contract/example/features/optional_result_virtual.cpp @@ -0,0 +1,88 @@ + +// 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 + +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <vector> +#include <cassert> + +template<typename T> +class accessible { +public: + virtual T& at(unsigned index, boost::contract::virtual_* v = 0) = 0; + + // Could program class invariants and contracts for following too. + virtual T const& operator[](unsigned index) const = 0; + virtual unsigned size() const = 0; +}; + +//[optional_result_virtual +template<typename T> +T& accessible<T>::at(unsigned index, boost::contract::virtual_* v) { + boost::optional<T&> result; + // Pass `result` right after `v`... + boost::contract::check c = boost::contract::public_function(v, result, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(index < size()); + }) + // ...plus postconditions take `result` as a parameter (not capture). + .postcondition([&] (boost::optional<T const&> const& result) { + BOOST_CONTRACT_ASSERT(*result == operator[](index)); + }) + ; + + assert(false); + return *result; +} +//] + +template<typename T> +class vector + #define BASES public accessible<T> + : BASES +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + T& at(unsigned index, boost::contract::virtual_* v = 0) /* override */ { + boost::optional<T&> result; + // Pass `result` right after `v`... + boost::contract::check c = boost::contract::public_function< + override_at>(v, result, &vector::at, this, index) + // ...plus postconditions take `result` as parameter (not capture). + .postcondition([&] (boost::optional<T const&> const& result) { + if(index == 0) BOOST_CONTRACT_ASSERT(*result == front()); + }) + ; + + return *(result = vect_[index]); + } + + // Could program class invariants and contracts for following too. + T const& operator[](unsigned index) const { return vect_[index]; } + unsigned size() const { return vect_.size(); } + T const& front() const { return vect_.front(); } + void push_back(T const& value) { vect_.push_back(value); } + + BOOST_CONTRACT_OVERRIDE(at) + +private: + std::vector<T> vect_; +}; + +int main() { + vector<int> v; + v.push_back(123); + v.push_back(456); + v.push_back(789); + int& x = v.at(1); + assert(x == 456); + x = -456; + assert(v.at(1) == -456); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/overload.cpp b/src/boost/libs/contract/example/features/overload.cpp new file mode 100644 index 000000000..2feab3478 --- /dev/null +++ b/src/boost/libs/contract/example/features/overload.cpp @@ -0,0 +1,202 @@ + +// 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 + +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <string> +#include <sstream> +#include <cassert> + +class lines { +public: + virtual std::string str(boost::contract::virtual_* v = 0) const = 0; + virtual std::string& str(boost::contract::virtual_* v = 0) = 0; + + virtual void put(std::string const& x, + boost::contract::virtual_* v = 0) = 0; + + virtual void put(char x, boost::contract::virtual_* v = 0) = 0; + + virtual void put(int x, bool tab = false, + boost::contract::virtual_* v = 0) = 0; +}; + +std::string lines::str(boost::contract::virtual_* v) const { + std::string result; + boost::contract::check c = boost::contract::public_function(v, result, this) + .postcondition([&] (std::string const& result) { + if(result != "") BOOST_CONTRACT_ASSERT(*result.rbegin() == '\n'); + }) + ; + assert(false); + return result; +} + +std::string& lines::str(boost::contract::virtual_* v) { + boost::optional<std::string&> result; + boost::contract::check c = boost::contract::public_function(v, result, this) + .postcondition([&] (boost::optional<std::string const&> const& result) { + if(*result != "") BOOST_CONTRACT_ASSERT(*result->rbegin() == '\n'); + }) + ; + assert(false); + return *result; +} + +void lines::put(std::string const& x, boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(*x.rbegin() != '\n'); + }) + ; + assert(false); +} + +void lines::put(char x, boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(x != '\n'); + }) + ; + assert(false); +} + +void lines::put(int x, bool tab, + boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(x >= 0); + }) + ; + assert(false); +} + +//[overload +class string_lines + #define BASES public lines + : BASES +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + BOOST_CONTRACT_OVERRIDES(str) // Invoked only once for all `str` overloads. + + std::string str(boost::contract::virtual_* v = 0) const /* override */ { + std::string result; + boost::contract::check c = boost::contract::public_function< + override_str>( + v, result, + // `static_cast` resolves overloaded function pointer ambiguities. + static_cast<std::string (string_lines::*)( + boost::contract::virtual_*) const>(&string_lines::str), + this + ); + + return result = str_; + } + + // Overload on (absence of) `const` qualifier. + std::string& str(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_str>( + v, str_, + // `static_cast` resolves overloaded function pointer ambiguities. + static_cast<std::string& (string_lines::*)( + boost::contract::virtual_*)>(&string_lines::str), + this + ); + + return str_; + } + + BOOST_CONTRACT_OVERRIDES(put) // Invoked only once for all `put` overloads. + + void put(std::string const& x, + boost::contract::virtual_* v = 0) /* override */ { + boost::contract::old_ptr<std::string> old_str = + BOOST_CONTRACT_OLDOF(v, str()); + boost::contract::check c = boost::contract::public_function< + override_put>( + v, + // `static_cast` resolves overloaded function pointer ambiguities. + static_cast<void (string_lines::*)(std::string const&, + boost::contract::virtual_*)>(&string_lines::put), + this, x + ) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(str() == *old_str + x + '\n'); + }) + ; + + str_ = str_ + x + '\n'; + } + + // Overload on argument type. + void put(char x, boost::contract::virtual_* v = 0) /* override */ { + boost::contract::old_ptr<std::string> old_str = + BOOST_CONTRACT_OLDOF(v, str()); + boost::contract::check c = boost::contract::public_function< + override_put>( + v, + // `static_cast` resolves overloaded function pointer ambiguities. + static_cast<void (string_lines::*)(char, + boost::contract::virtual_*)>(&string_lines::put), + this, x + ) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(str() == *old_str + x + '\n'); + }) + ; + + str_ = str_ + x + '\n'; + } + + // Overload on argument type and arity (also with default parameter). + void put(int x, bool tab = false, + boost::contract::virtual_* v = 0) /* override */ { + boost::contract::old_ptr<std::string> old_str = + BOOST_CONTRACT_OLDOF(v, str()); + boost::contract::check c = boost::contract::public_function< + override_put>( + v, + // `static_cast` resolves overloaded function pointer ambiguities. + static_cast<void (string_lines::*)(int, bool, + boost::contract::virtual_*)>(&string_lines::put), + this, x, tab + ) + .postcondition([&] { + std::ostringstream s; + s << x; + BOOST_CONTRACT_ASSERT( + str() == *old_str + (tab ? "\t" : "") + s.str() + '\n'); + }) + ; + + std::ostringstream s; + s << str_ << (tab ? "\t" : "") << x << '\n'; + str_ = s.str(); + } + +private: + std::string str_; +}; +//] + +int main() { + string_lines s; + s.put("abc"); + assert(s.str() == "abc\n"); + s.put('x'); + assert(s.str() == "abc\nx\n"); + s.put(10); + assert(s.str() == "abc\nx\n10\n"); + s.put(20, true); + lines const& l = s; + assert(l.str() == "abc\nx\n10\n\t20\n"); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/private_protected.cpp b/src/boost/libs/contract/example/features/private_protected.cpp new file mode 100644 index 000000000..7651a925b --- /dev/null +++ b/src/boost/libs/contract/example/features/private_protected.cpp @@ -0,0 +1,77 @@ + +// 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 + +#include <boost/contract.hpp> +#include <limits> +#include <cassert> + +//[private_protected +class counter { +protected: // Protected functions use `function()` (like non-members). + void set(int n) { + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(n <= 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == n); + }) + ; + + n_ = n; + } + +private: // Private functions use `function()` (like non-members). + void dec() { + boost::contract::old_ptr<int> old_get = BOOST_CONTRACT_OLDOF(get()); + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT( + get() + 1 >= std::numeric_limits<int>::min()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == *old_get - 1); + }) + ; + + set(get() - 1); + } + + int n_; + + /* ... */ +//] + +public: + int get() const { + int result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(result <= 0); + BOOST_CONTRACT_ASSERT(result == n_); + }) + ; + + return result = n_; + } + + counter() : n_(0) {} // Should contract constructor and destructor too. + + void invariant() const { + BOOST_CONTRACT_ASSERT(get() <= 0); + } + + friend int main(); +}; + +int main() { + counter cnt; + assert(cnt.get() == 0); + cnt.dec(); + assert(cnt.get() == -1); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/private_protected_virtual.cpp b/src/boost/libs/contract/example/features/private_protected_virtual.cpp new file mode 100644 index 000000000..534da5087 --- /dev/null +++ b/src/boost/libs/contract/example/features/private_protected_virtual.cpp @@ -0,0 +1,145 @@ + +// 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 + +#include <boost/contract.hpp> +#include <limits> +#include <cassert> + +//[private_protected_virtual_counter +class counter { + // Virtual private and protected functions still declare extra + // `virtual_* = 0` parameter (otherwise they cannot be overridden), but... +protected: + virtual void set(int n, boost::contract::virtual_* = 0) { + boost::contract::check c = boost::contract::function() // ...no `v`. + .precondition([&] { + BOOST_CONTRACT_ASSERT(n <= 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == n); + }) + ; + + n_ = n; + } + +private: + virtual void dec(boost::contract::virtual_* = 0) { + boost::contract::old_ptr<int> old_get = BOOST_CONTRACT_OLDOF(get()); // ...no `v`. + boost::contract::check c = boost::contract::function() // ...no `v`. + .precondition([&] { + BOOST_CONTRACT_ASSERT( + get() + 1 >= std::numeric_limits<int>::min()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == *old_get - 1); + }) + ; + + set(get() - 1); + } + + int n_; + + /* ... */ +//] + +public: + virtual int get(boost::contract::virtual_* v = 0) const { + int result; + boost::contract::check c = boost::contract::public_function( + v, result, this) + .postcondition([&] (int const result) { + BOOST_CONTRACT_ASSERT(result <= 0); + BOOST_CONTRACT_ASSERT(result == n_); + }) + ; + + return result = n_; + } + + counter() : n_(0) {} // Should contract constructor and destructor too. + + void invariant() const { + BOOST_CONTRACT_ASSERT(get() <= 0); + } + + friend int main(); +}; + +//[private_protected_virtual_counter10 +class counter10 + #define BASES public counter + : BASES +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + // Overriding from non-public members so no subcontracting, no override_... + + virtual void set(int n, boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(n % 10 == 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == n); + }) + ; + + counter::set(n); + } + + virtual void dec(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::old_ptr<int> old_get = BOOST_CONTRACT_OLDOF(v, get()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT( + get() + 10 >= std::numeric_limits<int>::min()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == *old_get - 10); + }) + ; + + set(get() - 10); + } + + /* ... */ +//] + + virtual int get(boost::contract::virtual_* v = 0) const { + int result; + boost::contract::check c = boost::contract::public_function< + override_get>(v, result, &counter10::get, this); + + return result = counter::get(); + } + BOOST_CONTRACT_OVERRIDE(get) + + // Should contract default constructor and destructor too. + + void invariant() const { + BOOST_CONTRACT_ASSERT(get() % 10 == 0); + } +}; + +int main() { + counter cnt; + assert(cnt.get() == 0); + cnt.dec(); + assert(cnt.get() == -1); + + counter10 cnt10; + counter& b = cnt10; // Polymorphic calls. + assert(b.get() == 0); + b.dec(); + assert(b.get() == -10); + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/private_protected_virtual_multi.cpp b/src/boost/libs/contract/example/features/private_protected_virtual_multi.cpp new file mode 100644 index 000000000..2ab875fbd --- /dev/null +++ b/src/boost/libs/contract/example/features/private_protected_virtual_multi.cpp @@ -0,0 +1,209 @@ + +// 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 + +#include <boost/config.hpp> +#ifdef BOOST_MSVC + +// WARNING: MSVC (at least up to VS 2015) gives a compile-time error if SFINAE +// cannot introspect a member because of its private or protected access level. +// That is incorrect, SFINAE should fail in these cases without generating +// compile-time errors like GCC and CLang do. Therefore, currently it is not +// possible to override a member that is public in one base but private or +// protected in other base using this library on MSVC (that can be done instead +// using this library on GCC or CLang). +int main() { return 0; } // Trivial program for MSVC. + +#else + +#include <boost/contract.hpp> +#include <limits> +#include <cassert> + +class counter { + // Virtual private and protected functions still declare extra + // `virtual_* = 0` parameter (otherwise they cannot be overridden). +protected: + virtual void set(int n, boost::contract::virtual_* = 0) { + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(n <= 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == n); + }) + ; + + n_ = n; + } + +private: + virtual void dec(boost::contract::virtual_* = 0) { + boost::contract::old_ptr<int> old_get = BOOST_CONTRACT_OLDOF(get()); + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT( + get() + 1 >= std::numeric_limits<int>::min()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == *old_get - 1); + }) + ; + + set(get() - 1); + } + + int n_; + +public: + virtual int get(boost::contract::virtual_* v = 0) const { + int result; + boost::contract::check c = boost::contract::public_function( + v, result, this) + .postcondition([&] (int const result) { + BOOST_CONTRACT_ASSERT(result <= 0); + BOOST_CONTRACT_ASSERT(result == n_); + }) + ; + + return result = n_; + } + + counter() : n_(0) {} // Should contract constructor and destructor too. + + void invariant() const { + BOOST_CONTRACT_ASSERT(get() <= 0); + } + + friend int main(); +}; + +//[private_protected_virtual_multi_countable +class countable { +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(get() <= 0); + } + + virtual void dec(boost::contract::virtual_* v = 0) = 0; + virtual void set(int n, boost::contract::virtual_* v = 0) = 0; + virtual int get(boost::contract::virtual_* v = 0) const = 0; +}; + +/* ... */ +//] + +void countable::dec(boost::contract::virtual_* v) { + boost::contract::old_ptr<int> old_get = BOOST_CONTRACT_OLDOF(v, get()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(get() > std::numeric_limits<int>::min()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() < *old_get); + }) + ; + assert(false); // Never executed by this library. +} + +void countable::set(int n, boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function( + v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(n <= 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == n); + }) + ; + assert(false); // Never executed by this library. +} + +int countable::get(boost::contract::virtual_* v) const { + int result; + boost::contract::check c = boost::contract::public_function( + v, result, this); + assert(false); // Never executed by this library. +} + +//[private_protected_virtual_multi_counter10 +class counter10 + #define BASES public countable, public counter // Multiple inheritance. + : BASES +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + // Overriding from public members from `countable` so use `override_...`. + + virtual void set(int n, boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_set>(v, &counter10::set, this, n) + .precondition([&] { + BOOST_CONTRACT_ASSERT(n % 10 == 0); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == n); + }) + ; + + counter::set(n); + } + + virtual void dec(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::old_ptr<int> old_get = BOOST_CONTRACT_OLDOF(v, get()); + boost::contract::check c = boost::contract::public_function< + override_dec>(v, &counter10::dec, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT( + get() + 10 >= std::numeric_limits<int>::min()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(get() == *old_get - 10); + }) + ; + + set(get() - 10); + } + + BOOST_CONTRACT_OVERRIDES(set, dec) + + /* ... */ +//] + + virtual int get(boost::contract::virtual_* v = 0) const { + int result; + boost::contract::check c = boost::contract::public_function< + override_get>(v, result, &counter10::get, this); + + return result = counter::get(); + } + BOOST_CONTRACT_OVERRIDE(get) + + // Should contract default constructor and destructor too. + + void invariant() const { + BOOST_CONTRACT_ASSERT(get() % 10 == 0); + } +}; + +int main() { + counter cnt; + assert(cnt.get() == 0); + cnt.dec(); + assert(cnt.get() == -1); + + counter10 cnt10; + countable& b = cnt10; // Polymorphic calls. + assert(b.get() == 0); + b.dec(); + assert(b.get() == -10); + + return 0; +} + +#endif // MSVC + diff --git a/src/boost/libs/contract/example/features/public.cpp b/src/boost/libs/contract/example/features/public.cpp new file mode 100644 index 000000000..a6d94aa72 --- /dev/null +++ b/src/boost/libs/contract/example/features/public.cpp @@ -0,0 +1,189 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <algorithm> +#include <cassert> + +//[public_class_begin +class unique_identifiers : + private boost::contract::constructor_precondition<unique_identifiers> +{ +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(size() >= 0); + } +//] + +//[public_constructor +public: + // Contract for a constructor. + unique_identifiers(int from, int to) : + boost::contract::constructor_precondition<unique_identifiers>([&] { + BOOST_CONTRACT_ASSERT(from >= 0); + BOOST_CONTRACT_ASSERT(to >= from); + }) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(size() == (to - from + 1)); + }) + ; + + // Constructor body. + for(int id = from; id <= to; ++id) vect_.push_back(id); + } +//] + +//[public_destructor +public: + // Contract for a destructor. + virtual ~unique_identifiers() { + // Following contract checks class invariants. + boost::contract::check c = boost::contract::destructor(this); + + // Destructor body here... (do nothing in this example). + } +//] + + int size() const { + // Following contract checks invariants. + boost::contract::check c = boost::contract::public_function(this); + return vect_.size(); + } + +//[public_function +public: + // Contract for a public function (but no static, virtual, or override). + bool find(int id) const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(id >= 0); + }) + .postcondition([&] { + if(size() == 0) BOOST_CONTRACT_ASSERT(!result); + }) + ; + + // Function body. + return result = std::find(vect_.begin(), vect_.end(), id) != + vect_.end(); + } +//] + +//[public_virtual_function +public: + // Contract for a public virtual function (but no override). + virtual int push_back(int id, boost::contract::virtual_* v = 0) { // Extra `v`. + int result; + boost::contract::old_ptr<bool> old_find = + BOOST_CONTRACT_OLDOF(v, find(id)); // Pass `v`. + boost::contract::old_ptr<int> old_size = + BOOST_CONTRACT_OLDOF(v, size()); // Pass `v`. + boost::contract::check c = boost::contract::public_function( + v, result, this) // Pass `v` and `result`. + .precondition([&] { + BOOST_CONTRACT_ASSERT(id >= 0); + BOOST_CONTRACT_ASSERT(!find(id)); // ID cannot be already present. + }) + .postcondition([&] (int const result) { + if(!*old_find) { + BOOST_CONTRACT_ASSERT(find(id)); + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + } + BOOST_CONTRACT_ASSERT(result == id); + }) + ; + + // Function body. + vect_.push_back(id); + return result = id; + } +//] + +private: + std::vector<int> vect_; +//[public_class_end + /* ... */ +}; +//] + +//[public_derived_class_begin +class identifiers + #define BASES public unique_identifiers + : BASES +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Bases typedef. + #undef BASES + + void invariant() const { // Check in AND with bases. + BOOST_CONTRACT_ASSERT(empty() == (size() == 0)); + } +//] + +//[public_function_override +public: + // Contract for a public function override. + int push_back(int id, boost::contract::virtual_* v = 0) /* override */ { + int result; + boost::contract::old_ptr<bool> old_find = + BOOST_CONTRACT_OLDOF(v, find(id)); + boost::contract::old_ptr<int> old_size = + BOOST_CONTRACT_OLDOF(v, size()); + boost::contract::check c = boost::contract::public_function< + override_push_back // Pass override type plus below function pointer... + >(v, result, &identifiers::push_back, this, id) // ...and arguments. + .precondition([&] { // Check in OR with bases. + BOOST_CONTRACT_ASSERT(id >= 0); + BOOST_CONTRACT_ASSERT(find(id)); // ID can be already present. + }) + .postcondition([&] (int const result) { // Check in AND with bases. + if(*old_find) BOOST_CONTRACT_ASSERT(size() == *old_size); + }) + ; + + // Function body. + if(!find(id)) unique_identifiers::push_back(id); // Else, do nothing. + return result = id; + } + BOOST_CONTRACT_OVERRIDE(push_back) // Define `override_push_back`. +//] + + bool empty() const { + // Following contract checks invariants. + boost::contract::check c = boost::contract::public_function(this); + return size() == 0; + } + + identifiers(int from, int to) : unique_identifiers(from, to) { + // Following contract checks invariants. + boost::contract::check c = boost::contract::constructor(this); + } + +//[public_derived_class_end + /* ... */ +}; +//] + +int main() { + unique_identifiers uids(1, 4); + assert(uids.find(2)); + assert(!uids.find(5)); + uids.push_back(5); + assert(uids.find(5)); + + identifiers ids(10, 40); + assert(!ids.find(50)); + ids.push_back(50); + ids.push_back(50); + assert(ids.find(50)); + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/pure_virtual_public.cpp b/src/boost/libs/contract/example/features/pure_virtual_public.cpp new file mode 100644 index 000000000..917a6c718 --- /dev/null +++ b/src/boost/libs/contract/example/features/pure_virtual_public.cpp @@ -0,0 +1,89 @@ + +// 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 + +#include <boost/contract.hpp> +#include <vector> +#include <cassert> + +//[pure_virtual_public_base_begin +template<typename Iterator> +class range { +public: + // Pure virtual function declaration (contract in definition below). + virtual Iterator begin(boost::contract::virtual_* v = 0) = 0; +//] + + // Could program class invariants and contracts for the following too. + virtual Iterator end() = 0; + virtual bool empty() const = 0; + +//[pure_virtual_public_base_end + /* ... */ +}; +//] + +//[pure_virtual_public_base_impl +// Pure virtual function default implementation (out-of-line in C++). +template<typename Iterator> +Iterator range<Iterator>::begin(boost::contract::virtual_* v) { + Iterator result; // As usual, virtual pass `result` right after `v`... + boost::contract::check c = boost::contract::public_function(v, result, this) + .postcondition([&] (Iterator const& result) { + if(empty()) BOOST_CONTRACT_ASSERT(result == end()); + }) + ; + + // Pure function body (never executed by this library). + assert(false); + return result; +} +//] + +template<typename T> +class vector + #define BASES public range<typename std::vector<T>::iterator> + : BASES +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + typedef typename std::vector<T>::iterator iterator; + + iterator begin(boost::contract::virtual_* v = 0) /* override */ { + iterator result; + // Again, pass result right after `v`... + boost::contract::check c = boost::contract::public_function< + override_begin>(v, result, &vector::begin, this) + // ...plus postconditions take `result` as parameter (not capture). + .postcondition([&] (iterator const& result) { + if(!empty()) BOOST_CONTRACT_ASSERT(*result == front()); + }) + ; + + return result = vect_.begin(); + } + BOOST_CONTRACT_OVERRIDE(begin) + + // Could program class invariants and contracts for the following too. + iterator end() { return vect_.end(); } + bool empty() const { return vect_.empty(); } + T const& front() const { return vect_.front(); } + void push_back(T const& value) { vect_.push_back(value); } + +private: + std::vector<T> vect_; +}; + +int main() { + vector<int> v; + v.push_back(1); + v.push_back(2); + v.push_back(3); + range<std::vector<int>::iterator>& r = v; + assert(*(r.begin()) == 1); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/separate_body.cpp b/src/boost/libs/contract/example/features/separate_body.cpp new file mode 100644 index 000000000..10e05b2ef --- /dev/null +++ b/src/boost/libs/contract/example/features/separate_body.cpp @@ -0,0 +1,36 @@ + +// 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 + +#include "separate_body.hpp" +#include <cassert> + +//[separate_body_cpp +void iarray::constructor_body(unsigned max, unsigned count) { + for(unsigned i = 0; i < count; ++i) values_[i] = int(); + size_ = count; +} + +void iarray::destructor_body() { delete[] values_; } + +void iarray::push_back_body(int value) { values_[size_++] = value; } + +/* ... */ +//] + +unsigned iarray::capacity_body() const { return capacity_; } +unsigned iarray::size_body() const { return size_; } + +int main() { + iarray a(3, 2); + assert(a.capacity() == 3); + assert(a.size() == 2); + + a.push_back(-123); + assert(a.size() == 3); + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/separate_body.hpp b/src/boost/libs/contract/example/features/separate_body.hpp new file mode 100644 index 000000000..6b83afd58 --- /dev/null +++ b/src/boost/libs/contract/example/features/separate_body.hpp @@ -0,0 +1,88 @@ + +#ifndef SEPARATE_BODY_HPP_ +#define SEPARATE_BODY_HPP_ + +// 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 + +#include <boost/contract.hpp> + +//[separate_body_hpp +class iarray : + private boost::contract::constructor_precondition<iarray> { +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(size() <= capacity()); + } + + explicit iarray(unsigned max, unsigned count = 0) : + boost::contract::constructor_precondition<iarray>([&] { + BOOST_CONTRACT_ASSERT(count <= max); + }), + // Still, member initializations must be here. + values_(new int[max]), + capacity_(max) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(capacity() == max); + BOOST_CONTRACT_ASSERT(size() == count); + }) + ; + constructor_body(max, count); // Separate constructor body impl. + } + + virtual ~iarray() { + boost::contract::check c = boost::contract::destructor(this); // Inv. + destructor_body(); // Separate destructor body implementation. + } + + virtual void push_back(int value, boost::contract::virtual_* v = 0) { + boost::contract::old_ptr<unsigned> old_size = + BOOST_CONTRACT_OLDOF(v, size()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(size() < capacity()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + }) + ; + push_back_body(value); // Separate member function body implementation. + } + +private: + // Contracts in class declaration (above), but body implementations are not. + void constructor_body(unsigned max, unsigned count); + void destructor_body(); + void push_back_body(int value); + + /* ... */ +//] + +public: + unsigned capacity() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return capacity_body(); + } + + unsigned size() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return size_body(); + } + +private: + unsigned size_body() const; + unsigned capacity_body() const; + + int* values_; + unsigned capacity_; + unsigned size_; +}; + +#endif // #include guard + diff --git a/src/boost/libs/contract/example/features/static_public.cpp b/src/boost/libs/contract/example/features/static_public.cpp new file mode 100644 index 000000000..146de0fa7 --- /dev/null +++ b/src/boost/libs/contract/example/features/static_public.cpp @@ -0,0 +1,69 @@ + +// 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 + +#include <boost/contract.hpp> +#include <cassert> + +//[static_public +template<class C> +class make { +public: + static void static_invariant() { // Static class invariants. + BOOST_CONTRACT_ASSERT(instances() >= 0); + } + + // Contract for a static public function. + static int instances() { + // Explicit template parameter `make` (check static invariants). + boost::contract::check c = boost::contract::public_function<make>(); + + return instances_; // Function body. + } + + /* ... */ +//] + + make() : object() { + boost::contract::old_ptr<int> old_instances = + BOOST_CONTRACT_OLDOF(instances()); + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(instances() == *old_instances + 1); + }) + ; + + ++instances_; + } + + ~make() { + boost::contract::old_ptr<int> old_instances = + BOOST_CONTRACT_OLDOF(instances()); + boost::contract::check c = boost::contract::destructor(this) + .postcondition([&] { // (An example of destructor postconditions.) + BOOST_CONTRACT_ASSERT(instances() == *old_instances - 1); + }) + ; + + --instances_; + } + + C object; + +private: + static int instances_; +}; + +template<class C> +int make<C>::instances_ = 0; + +int main() { + struct x {}; + make<x> x1, x2, x3; + assert(make<x>::instances() == 3); + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/throw_on_failure.cpp b/src/boost/libs/contract/example/features/throw_on_failure.cpp new file mode 100644 index 000000000..4cff315f2 --- /dev/null +++ b/src/boost/libs/contract/example/features/throw_on_failure.cpp @@ -0,0 +1,145 @@ + +// 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 + +#include <boost/contract.hpp> +#include <iostream> +#include <cstring> +#include <cassert> + +//[throw_on_failure_class_begin +struct too_large_error {}; + +template<unsigned MaxSize> +class cstring + #define BASES private boost::contract::constructor_precondition<cstring< \ + MaxSize> > + : BASES +{ +//] +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + +//[throw_on_failure_ctor +public: + /* implicit */ cstring(char const* chars) : + boost::contract::constructor_precondition<cstring>([&] { + BOOST_CONTRACT_ASSERT(chars); // Throw `assertion_failure`. + // Or, throw user-defined exception. + if(std::strlen(chars) > MaxSize) throw too_large_error(); + }) + { +//] + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(size() == std::strlen(chars)); + }) + ; + + size_ = std::strlen(chars); + for(unsigned i = 0; i < size_; ++i) chars_[i] = chars[i]; + chars_[size_] = '\0'; + } + +//[throw_on_failure_dtor +public: + void invariant() const { + if(size() > MaxSize) throw too_large_error(); // Throw user-defined ex. + BOOST_CONTRACT_ASSERT(chars_); // Or, throw `assertion_failure`. + BOOST_CONTRACT_ASSERT(chars_[size()] == '\0'); + } + + ~cstring() noexcept { // Exception specifiers apply to contract code. + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } +//] + + unsigned size() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return size_; + } + +private: + char chars_[MaxSize + 1]; + unsigned size_; +//[throw_on_failure_class_end + /* ... */ +}; +//] + +void bad_throwing_handler() { // For docs only (not actually used here). + //[throw_on_failure_bad_handler + /* ... */ + + // Warning... might cause destructors to throw (unless declared noexcept). + boost::contract::set_invariant_failure( + [] (boost::contract::from) { + throw; // Throw no matter if from destructor, etc. + } + ); + + /* ... */ + //] +} + +//[throw_on_failure_handlers +int main() { + boost::contract::set_precondition_failure( + boost::contract::set_postcondition_failure( + boost::contract::set_invariant_failure( + boost::contract::set_old_failure( + [] (boost::contract::from where) { + if(where == boost::contract::from_destructor) { + // Shall not throw from C++ destructors. + std::clog << "ignored destructor contract failure" << std::endl; + } else throw; // Re-throw (assertion_failure, user-defined, etc.). + } + )))); + boost::contract::set_except_failure( + [] (boost::contract::from) { + // Already an active exception so shall not throw another... + std::clog << "ignored exception guarantee failure" << std::endl; + } + ); + boost::contract::set_check_failure( + [] { + // But now CHECK shall not be used in destructor implementations. + throw; // Re-throw (assertion_failure, user-defined, etc.). + } + ); + + /* ... */ +//] + + { + cstring<3> s("abc"); + assert(s.size() == 3); + } + + #ifndef BOOST_CONTRACT_NO_PRECONDITIONS + // These failures properly handled only when preconditions checked. + + try { + char* c = 0; + cstring<3> s(c); + assert(false); + } catch(boost::contract::assertion_failure const& error) { + // OK (expected). + std::clog << "ignored: " << error.what() << std::endl; + } catch(...) { assert(false); } + + try { + cstring<3> s("abcd"); + assert(false); + } catch(too_large_error const&) {} // OK (expected). + catch(...) { assert(false); } + #endif + + return 0; +} + diff --git a/src/boost/libs/contract/example/features/union.cpp b/src/boost/libs/contract/example/features/union.cpp new file mode 100644 index 000000000..0681c774e --- /dev/null +++ b/src/boost/libs/contract/example/features/union.cpp @@ -0,0 +1,134 @@ + +// 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 + +#include <boost/contract.hpp> +#include <boost/config.hpp> +#include <cassert> + +#ifdef BOOST_GCC // G++ does not support static union members yet. + int instances_ = 0; +#endif + +//[union +union positive { +public: + static void static_invariant() { // Static class invariants (as usual). + BOOST_CONTRACT_ASSERT(instances() >= 0); + } + + void invariant() const { // Class invariants (as usual). + BOOST_CONTRACT_ASSERT(i_ > 0); + BOOST_CONTRACT_ASSERT(d_ > 0); + } + + // Contracts for constructor, as usual but... + explicit positive(int x) : d_(0) { + // ...unions cannot have bases so constructor preconditions here. + boost::contract::constructor_precondition<positive> pre([&] { + BOOST_CONTRACT_ASSERT(x > 0); + }); + boost::contract::old_ptr<int> old_instances = + BOOST_CONTRACT_OLDOF(instances()); + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + { int y; get(y); BOOST_CONTRACT_ASSERT(y == x); } + BOOST_CONTRACT_ASSERT(instances() == *old_instances + 1); + }) + ; + + i_ = x; + ++instances_; + } + + // Contracts for destructor (as usual). + ~positive() { + boost::contract::old_ptr<int> old_instances = + BOOST_CONTRACT_OLDOF(instances()); + boost::contract::check c = boost::contract::destructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(instances() == *old_instances - 1); + }) + ; + + --instances_; + } + + // Contracts for public function (as usual, but no virtual or override). + void get(int& x) const { + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(x > 0); + }) + ; + + x = i_; + } + + // Contracts for static public function (as usual). + static int instances() { + boost::contract::check c = boost::contract::public_function<positive>(); + return instances_; + } + +private: + int i_; + double d_; + + /* ... */ +//] + +public: + explicit positive(double x) : d_(0) { + // Unions cannot have bases so constructor preconditions here. + boost::contract::constructor_precondition<positive> pre([&] { + BOOST_CONTRACT_ASSERT(x > 0); + }); + boost::contract::old_ptr<int> old_instances = + BOOST_CONTRACT_OLDOF(instances()); + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + { double y; get(y); BOOST_CONTRACT_ASSERT(y == x); } + BOOST_CONTRACT_ASSERT(instances() == *old_instances + 1); + }) + ; + + d_ = x; + ++instances_; + } + + void get(double& x) const { + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(x > 0); + }) + ; + + x = d_; + } + + #ifndef BOOST_GCC // G++ does not support static union members yet. + static int instances_; + #endif +}; + +#ifndef BOOST_GCC // G++ does not support static union members yet. + int positive::instances_ = 0; +#endif + +int main() { + { + positive p(123); + assert(p.instances() == 1); + { int y = -456; p.get(y); assert(y == 123); } + + positive q(1.23); + assert(q.instances() == 2); + { double y = -4.56; q.get(y); assert(y == 1.23); } + } + assert(positive::instances() == 0); + return 0; +} + diff --git a/src/boost/libs/contract/example/features/volatile.cpp b/src/boost/libs/contract/example/features/volatile.cpp new file mode 100644 index 000000000..eb9b2e710 --- /dev/null +++ b/src/boost/libs/contract/example/features/volatile.cpp @@ -0,0 +1,102 @@ + +// 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 + +#include <boost/contract.hpp> +#include <cassert> + +//[volatile +class u { +public: + static void static_invariant(); // Static invariants. + void invariant() const volatile; // Volatile invariants. + void invariant() const; // Const invariants. + + u() { // Check static, volatile, and const invariants. + boost::contract::check c= boost::contract::constructor(this); + } + + ~u() { // Check static, volatile, and const invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + void nc() { // Check static and const invariants. + boost::contract::check c = boost::contract::public_function(this); + } + + void c() const { // Check static and const invariants. + boost::contract::check c = boost::contract::public_function(this); + } + + void v() volatile { // Check static and volatile invariants. + boost::contract::check c = boost::contract::public_function(this); + } + + void cv() const volatile { // Check static and volatile invariants. + boost::contract::check c = boost::contract::public_function(this); + } + + static void s() { // Check static invariants only. + boost::contract::check c = boost::contract::public_function<u>(); + } +}; +//] + +bool static_inv_checked, cv_inv_checked, const_inv_checked; +void u::static_invariant() { static_inv_checked = true; } +void u::invariant() const volatile { cv_inv_checked = true; } +void u::invariant() const { const_inv_checked = true; } + +int main() { + #ifndef BOOST_CONTRACT_NO_EXIT_INVARIANTS + { + static_inv_checked = cv_inv_checked = const_inv_checked = false; + u x; + assert(static_inv_checked); + assert(cv_inv_checked); + assert(const_inv_checked); + + static_inv_checked = cv_inv_checked = const_inv_checked = false; + x.nc(); + assert(static_inv_checked); + assert(!cv_inv_checked); + assert(const_inv_checked); + + static_inv_checked = cv_inv_checked = const_inv_checked = false; + x.c(); + assert(static_inv_checked); + assert(!cv_inv_checked); + assert(const_inv_checked); + + static_inv_checked = cv_inv_checked = const_inv_checked = false; + x.v(); + assert(static_inv_checked); + assert(cv_inv_checked); + assert(!const_inv_checked); + + static_inv_checked = cv_inv_checked = const_inv_checked = false; + x.cv(); + assert(static_inv_checked); + assert(cv_inv_checked); + assert(!const_inv_checked); + + static_inv_checked = cv_inv_checked = const_inv_checked = false; + x.s(); + assert(static_inv_checked); + assert(!cv_inv_checked); + assert(!const_inv_checked); + + static_inv_checked = cv_inv_checked = const_inv_checked = false; + } // Call destructor. + #ifndef BOOST_CONTRACT_NO_ENTRY_INVARIANTS + assert(static_inv_checked); + assert(cv_inv_checked); + assert(const_inv_checked); + #endif + #endif + + return 0; +} + diff --git a/src/boost/libs/contract/example/meyer97/stack3.cpp b/src/boost/libs/contract/example/meyer97/stack3.cpp new file mode 100644 index 000000000..0da895b4f --- /dev/null +++ b/src/boost/libs/contract/example/meyer97/stack3.cpp @@ -0,0 +1,192 @@ + +// 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 + +//[meyer97_stack3 +// File: stack3.cpp +#include "stack4.hpp" +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <cassert> + +// Dispenser LIFO with max capacity using error codes. +template<typename T> +class stack3 { + friend class boost::contract::access; + + void invariant() const { + if(!error()) { + BOOST_CONTRACT_ASSERT(count() >= 0); // Count non-negative. + BOOST_CONTRACT_ASSERT(count() <= capacity()); // Count bounded. + // Empty if no element. + BOOST_CONTRACT_ASSERT(empty() == (count() == 0)); + } + } + +public: + enum error_code { + no_error = 0, + overflow_error, + underflow_error, + size_error + }; + + /* Initialization */ + + // Create stack for max of n elems, if n < 0 set error (no preconditions). + explicit stack3(int n, T const& default_value = T()) : + stack_(0), error_(no_error) { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + // Error if impossible. + BOOST_CONTRACT_ASSERT((n < 0) == (error() == size_error)); + // No error if possible. + BOOST_CONTRACT_ASSERT((n >= 0) == !error()); + // Created if no error. + if(!error()) BOOST_CONTRACT_ASSERT(capacity() == n); + }) + ; + + if(n >= 0) stack_ = stack4<T>(n); + else error_ = size_error; + } + + /* Access */ + + // Max number of stack elements. + int capacity() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return stack_.capacity(); + } + + // Number of stack elements. + int count() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return stack_.count(); + } + + // Top element if present, otherwise none and set error (no preconditions). + boost::optional<T const&> item() const { + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Error if impossible. + BOOST_CONTRACT_ASSERT(empty() == (error() == underflow_error)); + // No error if possible. + BOOST_CONTRACT_ASSERT(!empty() == !error()); + }) + ; + + if(!empty()) { + error_ = no_error; + return boost::optional<T const&>(stack_.item()); + } else { + error_ = underflow_error; + return boost::optional<T const&>(); + } + } + + /* Status Report */ + + // Error indicator set by various operations. + error_code error() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return error_; + } + + bool empty() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return stack_.empty(); + } + + bool full() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return stack_.full(); + } + + /* Element Change */ + + // Add x to top if capacity allows, otherwise set error (no preconditions). + void put(T const& x) { + boost::contract::old_ptr<bool> old_full = BOOST_CONTRACT_OLDOF(full()); + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Error if impossible. + BOOST_CONTRACT_ASSERT(*old_full == (error() == overflow_error)); + // No error if possible. + BOOST_CONTRACT_ASSERT(!*old_full == !error()); + if(!error()) { // If no error... + BOOST_CONTRACT_ASSERT(!empty()); // ...not empty. + BOOST_CONTRACT_ASSERT(*item() == x); // ...added to top. + // ...one more. + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); + } + }) + ; + + if(full()) error_ = overflow_error; + else { + stack_.put(x); + error_ = no_error; + } + } + + // Remove top element if possible, otherwise set error (no preconditions). + void remove() { + boost::contract::old_ptr<bool> old_empty = + BOOST_CONTRACT_OLDOF(empty()); + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Error if impossible. + BOOST_CONTRACT_ASSERT(*old_empty == (error() == + underflow_error)); + // No error if possible. + BOOST_CONTRACT_ASSERT(!*old_empty == !error()); + if(!error()) { // If no error... + BOOST_CONTRACT_ASSERT(!full()); // ...not full. + // ...one less. + BOOST_CONTRACT_ASSERT(count() == *old_count - 1); + } + }) + ; + + if(empty()) error_ = underflow_error; + else { + stack_.remove(); + error_ = no_error; + } + } + +private: + stack4<T> stack_; + mutable error_code error_; +}; + +int main() { + stack3<int> s(3); + assert(s.capacity() == 3); + assert(s.count() == 0); + assert(s.empty()); + assert(!s.full()); + + s.put(123); + assert(!s.empty()); + assert(!s.full()); + assert(*s.item() == 123); + + s.remove(); + assert(s.empty()); + assert(!s.full()); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/meyer97/stack4.e b/src/boost/libs/contract/example/meyer97/stack4.e new file mode 100644 index 000000000..85d6e539d --- /dev/null +++ b/src/boost/libs/contract/example/meyer97/stack4.e @@ -0,0 +1,201 @@ + +-- 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 + +//[meyer97_stack4_e +-- 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. +//] + diff --git a/src/boost/libs/contract/example/meyer97/stack4.hpp b/src/boost/libs/contract/example/meyer97/stack4.hpp new file mode 100644 index 000000000..541625cc9 --- /dev/null +++ b/src/boost/libs/contract/example/meyer97/stack4.hpp @@ -0,0 +1,201 @@ + +// 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 + +//[meyer97_stack4 +// 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 +//] + diff --git a/src/boost/libs/contract/example/meyer97/stack4_main.cpp b/src/boost/libs/contract/example/meyer97/stack4_main.cpp new file mode 100644 index 000000000..0ea28896e --- /dev/null +++ b/src/boost/libs/contract/example/meyer97/stack4_main.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 + +//[meyer97_stack4_main +#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; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/counter/counter.hpp b/src/boost/libs/contract/example/mitchell02/counter/counter.hpp new file mode 100644 index 000000000..659edbe9f --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/counter/counter.hpp @@ -0,0 +1,71 @@ + +// 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 + +//[mitchell02_counter +#ifndef COUNTER_HPP_ +#define COUNTER_HPP_ + +#include "../observer/subject.hpp" +#include <boost/contract.hpp> + +class counter + #define BASES public subject + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + +public: + /* Creation */ + + // Construct counter with specified value. + explicit counter(int a_value = 10) : value_(a_value) { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(value() == a_value); // Value set. + }) + ; + } + + // Destroy counter. + virtual ~counter() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Queries */ + + // Current counter value. + int value() const { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::public_function(this); + return value_; + } + + /* Commands */ + + // Decrement counter value. + void decrement() { + boost::contract::old_ptr<int> old_value = BOOST_CONTRACT_OLDOF(value()); + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(value() == *old_value - 1); // Decrement. + }) + ; + + --value_; + notify(); // Notify all attached observers. + } + +private: + int value_; +}; + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/counter/decrement_button.hpp b/src/boost/libs/contract/example/mitchell02/counter/decrement_button.hpp new file mode 100644 index 000000000..ba8ae67e9 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/counter/decrement_button.hpp @@ -0,0 +1,94 @@ + +// 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 + +//[mitchell02_decrement_button +#ifndef DECREMENT_BUTTON_HPP_ +#define DECREMENT_BUTTON_HPP_ + +#include "push_button.hpp" +#include "counter.hpp" +#include "../observer/observer.hpp" +#include <boost/contract.hpp> +#include <boost/noncopyable.hpp> + +class decrement_button + #define BASES public push_button, public observer, \ + private boost::noncopyable + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + BOOST_CONTRACT_OVERRIDES(on_bn_clicked, up_to_date_with_subject, update); + +public: + /* Creation */ + + explicit decrement_button(counter& a_counter) : counter_(a_counter) { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + // Enable iff positive value. + BOOST_CONTRACT_ASSERT(enabled() == (a_counter.value() > 0)); + }) + ; + counter_.attach(this); + } + + // Destroy button. + virtual ~decrement_button() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Commands */ + + virtual void on_bn_clicked(boost::contract::virtual_* v = 0) + /* override */ { + boost::contract::old_ptr<int> old_value = + BOOST_CONTRACT_OLDOF(v, counter_.value()); + boost::contract::check c = boost::contract::public_function< + override_on_bn_clicked + >(v, &decrement_button::on_bn_clicked, this) + .postcondition([&] { + // Counter decremented. + BOOST_CONTRACT_ASSERT(counter_.value() == *old_value - 1); + }) + ; + counter_.decrement(); + } + + virtual bool up_to_date_with_subject(boost::contract::virtual_* v = 0) + const /* override */ { + bool result; + boost::contract::check c = boost::contract::public_function< + override_up_to_date_with_subject + >(v, result, &decrement_button::up_to_date_with_subject, this); + + return result = true; // For simplicity, assume always up-to-date. + } + + virtual void update(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_update>(v, &decrement_button::update, this) + .postcondition([&] { + // Enabled iff positive value. + BOOST_CONTRACT_ASSERT(enabled() == (counter_.value() > 0)); + }) + ; + + if(counter_.value() == 0) disable(); + else enable(); + } + +private: + counter& counter_; +}; + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/counter/push_button.hpp b/src/boost/libs/contract/example/mitchell02/counter/push_button.hpp new file mode 100644 index 000000000..eaa66f79d --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/counter/push_button.hpp @@ -0,0 +1,86 @@ + +// 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 + +//[mitchell02_push_button +#ifndef PUSH_BUTTON_HPP_ +#define PUSH_BUTTON_HPP_ + +#include <boost/contract.hpp> +#include <cassert> + +class push_button { +public: + // No inv and no bases so contracts optional if no pre, post, and override. + + /* Creation */ + + // Create an enabled button. + push_button() : enabled_(true) { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(enabled()); // Enabled. + }) + ; + } + + // Destroy button. + virtual ~push_button() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Queries */ + + // If button is enabled. + bool enabled() const { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::public_function(this); + return enabled_; + } + + /* Commands */ + + // Enable button. + void enable() { + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(enabled()); // Enabled. + }) + ; + + enabled_ = true; + } + + // Disable button. + void disable() { + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!enabled()); // Disabled. + }) + ; + + enabled_ = false; + } + + // Invoke externally when button clicked. + virtual void on_bn_clicked(boost::contract::virtual_* v = 0) = 0; + +private: + bool enabled_; +}; + +void push_button::on_bn_clicked(boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(enabled()); // Enabled. + }) + ; + assert(false); +} + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/counter_main.cpp b/src/boost/libs/contract/example/mitchell02/counter_main.cpp new file mode 100644 index 000000000..ace7b8b92 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/counter_main.cpp @@ -0,0 +1,81 @@ + +// 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 + +//[mitchell02_counter_main +#include "counter/counter.hpp" +#include "counter/decrement_button.hpp" +#include "observer/observer.hpp" +#include <cassert> + +int test_counter; + +class view_of_counter + #define BASES public observer + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + BOOST_CONTRACT_OVERRIDES(up_to_date_with_subject, update) + +public: + /* Creation */ + + // Create view associated with given counter. + explicit view_of_counter(counter& a_counter) : counter_(a_counter) { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::constructor(this); + + counter_.attach(this); + assert(counter_.value() == test_counter); + } + + // Destroy view. + virtual ~view_of_counter() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Commands */ + + virtual bool up_to_date_with_subject(boost::contract::virtual_* v = 0) + const /* override */ { + bool result; + boost::contract::check c = boost::contract::public_function< + override_up_to_date_with_subject + >(v, result, &view_of_counter::up_to_date_with_subject, this); + + return result = true; // For simplicity, assume always up-to-date. + } + + virtual void update(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_update>(v, &view_of_counter::update, this); + + assert(counter_.value() == test_counter); + } + +private: + counter& counter_; +}; + +int main() { + counter cnt(test_counter = 1); + view_of_counter view(cnt); + + decrement_button dec(cnt); + assert(dec.enabled()); + + test_counter--; + dec.on_bn_clicked(); + assert(!dec.enabled()); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/courier.cpp b/src/boost/libs/contract/example/mitchell02/courier.cpp new file mode 100644 index 000000000..e04fa0d9e --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/courier.cpp @@ -0,0 +1,207 @@ + +// 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 + +//[mitchell02_courier +#include <boost/contract.hpp> +#include <string> +#include <cassert> + +struct package { + double weight_kg; + std::string location; + double accepted_hour; + double delivered_hour; + + explicit package( + double _weight_kg, + std::string const& _location = "", + double _accepted_hour = 0.0, + double _delivered_hour = 0.0 + ) : + weight_kg(_weight_kg), + location(_location), + accepted_hour(_accepted_hour), + delivered_hour(_delivered_hour) + {} +}; + +// Courier for package delivery. +class courier + #define BASES private boost::contract::constructor_precondition<courier> + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + static void static_invariant() { + // Positive min. insurance. + BOOST_CONTRACT_ASSERT(min_insurance_usd >= 0.0); + } + + void invariant() const { + // Above min. insurance. + BOOST_CONTRACT_ASSERT(insurance_cover_usd() >= min_insurance_usd); + } + +public: + static double min_insurance_usd; + + /* Creation */ + + // Create courier with specified insurance value. + explicit courier(double _insurance_cover_usd = min_insurance_usd) : + boost::contract::constructor_precondition<courier>([&] { + // Positive insurance. + BOOST_CONTRACT_ASSERT(_insurance_cover_usd >= 0.0); + }), + insurance_cover_usd_(_insurance_cover_usd) + { + // Check invariants. + boost::contract::check c = boost::contract::constructor(this); + } + + // Destroy courier. + virtual ~courier() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Queries */ + + // Return insurance cover. + double insurance_cover_usd() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return insurance_cover_usd_; + } + + /* Commands */ + + // Deliver package to destination. + virtual void deliver( + package& package_delivery, + std::string const& destination, + boost::contract::virtual_* v = 0 + ) { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + // Within max weight of this delivery. + BOOST_CONTRACT_ASSERT(package_delivery.weight_kg < 5.0); + }) + .postcondition([&] { + // Within max delivery type. + BOOST_CONTRACT_ASSERT(double(package_delivery.delivered_hour - + package_delivery.accepted_hour) <= 3.0); + // Delivered at destination. + BOOST_CONTRACT_ASSERT(package_delivery.location == destination); + }) + ; + + package_delivery.location = destination; + // Delivery takes 2.5 hours. + package_delivery.delivered_hour = package_delivery.accepted_hour + 2.5; + } + +private: + double insurance_cover_usd_; +}; + +double courier::min_insurance_usd = 10.0e+6; + +// Different courier for package delivery. +class different_courier + #define BASES private boost::contract::constructor_precondition< \ + different_courier>, public courier + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. + #undef BASES + + static void static_invariant() { + BOOST_CONTRACT_ASSERT( // Better insurance amount. + different_insurance_usd >= courier::min_insurance_usd); + } + + void invariant() const { + // Above different insurance value. + BOOST_CONTRACT_ASSERT(insurance_cover_usd() >= different_insurance_usd); + } + + BOOST_CONTRACT_OVERRIDE(deliver) + +public: + static double different_insurance_usd; + + /* Creation */ + + // Create courier with specified insurance value. + explicit different_courier( + double insurance_cover_usd = different_insurance_usd) : + boost::contract::constructor_precondition<different_courier>([&] { + // Positive insurance value. + BOOST_CONTRACT_ASSERT(insurance_cover_usd > 0.0); + }), + courier(insurance_cover_usd) + { + // Check invariants. + boost::contract::check c = boost::contract::constructor(this); + } + + // Destroy courier. + virtual ~different_courier() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Commands */ + + virtual void deliver( + package& package_delivery, + std::string const& destination, + boost::contract::virtual_* v = 0 + ) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_deliver + >(v, &different_courier::deliver, this, package_delivery, destination) + .precondition([&] { + // Package can weight more (weaker precondition). + BOOST_CONTRACT_ASSERT(package_delivery.weight_kg <= 8.0); + }) + .postcondition([&] { + // Faster delivery (stronger postcondition). + BOOST_CONTRACT_ASSERT(double(package_delivery.delivered_hour - + package_delivery.accepted_hour) <= 2.0); + // Inherited "delivery at destination" postcondition. + }) + ; + + package_delivery.location = destination; + // Delivery takes 0.5 hours. + package_delivery.delivered_hour = package_delivery.accepted_hour + 0.5; + } +}; + +double different_courier::different_insurance_usd = 20.0e+6; + +int main() { + package cups(3.6, "store"); + courier c; + c.deliver(cups, "home"); + assert(cups.location == "home"); + + package desk(7.2, "store"); + different_courier dc; + dc.deliver(desk, "office"); + assert(desk.location == "office"); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/customer_manager.cpp b/src/boost/libs/contract/example/mitchell02/customer_manager.cpp new file mode 100644 index 000000000..1d92120a3 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/customer_manager.cpp @@ -0,0 +1,137 @@ + +// 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 + +//[mitchell02_customer_manager +#include <boost/contract.hpp> +#include <string> +#include <map> +#include <utility> +#include <cassert> + +// Basic customer information. +struct customer_info { + friend class customer_manager; + + typedef std::string identifier; + + identifier id; + + explicit customer_info(identifier const& _id) : + id(_id), name_(), address_(), birthday_() {} + +private: + std::string name_; + std::string address_; + std::string birthday_; +}; + +// Manage customers. +class customer_manager { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. + } + +public: + /* Creation */ + + customer_manager() { + // Check invariants. + boost::contract::check c = boost::contract::constructor(this); + } + + virtual ~customer_manager() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Basic Queries */ + + int count() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return customers_.size(); + } + + bool id_active(customer_info::identifier const& id) const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return customers_.find(id) != customers_.cend(); + } + + /* Derived Queries */ + + std::string const& name_for(customer_info::identifier const& id) const { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(id_active(id)); // Active. + }) + ; + + // Find != end because of preconditions (no defensive programming). + return customers_.find(id)->second.name_; + } + + /* Commands */ + + void add(customer_info const& info) { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + // Not already active. + BOOST_CONTRACT_ASSERT(!id_active(info.id)); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc. + BOOST_CONTRACT_ASSERT(id_active(info.id)); // Activated. + }) + ; + + customers_.insert(std::make_pair(info.id, customer(info))); + } + + void set_name(customer_info::identifier const& id, + std::string const& name) { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(id_active(id)); // Already active. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(name_for(id) == name); // Name set. + }) + ; + + // Find != end because of precondition (no defensive programming). + customers_.find(id)->second.name_ = name; + } + +private: + class agent {}; // Customer agent. + + struct customer : customer_info { + agent managing_agent; + std::string last_contact; + + explicit customer(customer_info const& info) : customer_info(info), + managing_agent(), last_contact() {} + }; + + std::map<customer_info::identifier, customer> customers_; +}; + +int main() { + customer_manager m; + customer_info const js("john_smith_123"); + m.add(js); + m.set_name(js.id, "John Smith"); + assert(m.name_for(js.id) == "John Smith"); + assert(m.count() == 1); + assert(m.id_active(js.id)); + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/dictionary.cpp b/src/boost/libs/contract/example/mitchell02/dictionary.cpp new file mode 100644 index 000000000..c2731a38f --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/dictionary.cpp @@ -0,0 +1,128 @@ + +// 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 + +//[mitchell02_dictionary +#include <boost/contract.hpp> +#include <utility> +#include <map> +#include <cassert> + +template<typename K, typename T> +class dictionary { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. + } + +public: + /* Creation */ + + // Create empty dictionary. + dictionary() { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == 0); // Empty. + }) + ; + } + + // Destroy dictionary. + virtual ~dictionary() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Basic Queries */ + + // Number of key entries. + int count() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return items_.size(); + } + + // Has entry for key? + bool has(K const& key) const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Empty has no key. + if(count() == 0) BOOST_CONTRACT_ASSERT(!result); + }) + ; + + return result = (items_.find(key) != items_.end()); + } + + // Value for a given key. + T const& value_for(K const& key) const { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(has(key)); // Has key. + }) + ; + + // Find != end because of precondition (no defensive programming). + return items_.find(key)->second; + } + + /* Commands */ + + // Add value of a given key. + void put(K const& key, T const& value) { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!has(key)); // Has not key already. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc. + BOOST_CONTRACT_ASSERT(has(key)); // Has key. + // Value set for key. + BOOST_CONTRACT_ASSERT(value_for(key) == value); + }) + ; + + items_.insert(std::make_pair(key, value)); + } + + // Remove value for given key. + void remove(K const& key) { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(has(key)); // Has key. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec. + BOOST_CONTRACT_ASSERT(!has(key)); // Has not key. + }) + ; + + items_.erase(key); + } + +private: + std::map<K, T> items_; +}; + +int main() { + std::string const js = "John Smith"; + + dictionary<std::string, int> ages; + assert(!ages.has(js)); + + ages.put(js, 23); + assert(ages.value_for(js) == 23); + + ages.remove(js); + assert(ages.count() == 0); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/name_list.cpp b/src/boost/libs/contract/example/mitchell02/name_list.cpp new file mode 100644 index 000000000..fa394ed59 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/name_list.cpp @@ -0,0 +1,145 @@ + +// 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 + +//[mitchell02_name_list +#include <boost/contract.hpp> +#include <string> +#include <vector> +#include <algorithm> +#include <cassert> + +// List of names. +class name_list { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. + } + +public: + /* Creation */ + + // Create an empty list. + name_list() { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == 0); // Empty list. + }) + ; + } + + // Destroy list. + virtual ~name_list() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Basic Queries */ + + // Number of names in list. + int count() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return names_.size(); + } + + // Is name in list? + bool has(std::string const& name) const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // If empty, has not. + if(count() == 0) BOOST_CONTRACT_ASSERT(!result); + }) + ; + + return result = names_.cend() != std::find(names_.cbegin(), + names_.cend(), name); + } + + /* Commands */ + + // Add name to list, if name not already in list. + virtual void put(std::string const& name, + boost::contract::virtual_* v = 0) { + boost::contract::old_ptr<bool> old_has_name = + BOOST_CONTRACT_OLDOF(v, has(name)); + boost::contract::old_ptr<int> old_count = + BOOST_CONTRACT_OLDOF(v, count()); + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!has(name)); // Not already in list. + }) + .postcondition([&] { + if(!*old_has_name) { // If-guard allows to relax subcontracts. + BOOST_CONTRACT_ASSERT(has(name)); // Name in list. + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Inc. + } + }) + ; + + names_.push_back(name); + } + +private: + std::vector<std::string> names_; +}; + +class relaxed_name_list + #define BASES public name_list + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. + #undef BASES + + BOOST_CONTRACT_OVERRIDE(put); + +public: + /* Commands */ + + // Add name to list, or do nothing if name already in list (relaxed). + void put(std::string const& name, + boost::contract::virtual_* v = 0) /* override */ { + boost::contract::old_ptr<bool> old_has_name = + BOOST_CONTRACT_OLDOF(v, has(name)); + boost::contract::old_ptr<int> old_count = + BOOST_CONTRACT_OLDOF(v, count()); + boost::contract::check c = boost::contract::public_function< + override_put>(v, &relaxed_name_list::put, this, name) + .precondition([&] { // Relax inherited preconditions. + BOOST_CONTRACT_ASSERT(has(name)); // Already in list. + }) + .postcondition([&] { // Inherited post. not checked given if-guard. + if(*old_has_name) { + // Count unchanged if name already in list. + BOOST_CONTRACT_ASSERT(count() == *old_count); + } + }) + ; + + if(!has(name)) name_list::put(name); // Else, do nothing. + } +}; + +int main() { + std::string const js = "John Smith"; + + relaxed_name_list rl; + rl.put(js); + assert(rl.has(js)); + rl.put(js); // OK, relaxed contracts allow calling this again (do nothing). + + name_list nl; + nl.put(js); + assert(nl.has(js)); + // nl.put(js); // Error, contracts do not allow calling this again. + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/observer/observer.hpp b/src/boost/libs/contract/example/mitchell02/observer/observer.hpp new file mode 100644 index 000000000..aa8a91ed0 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/observer/observer.hpp @@ -0,0 +1,59 @@ + +// 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 + +//[mitchell02_observer +#ifndef OBSERVER_HPP_ +#define OBSERVER_HPP_ + +#include <boost/contract.hpp> +#include <cassert> + +// Observer. +class observer { + friend class subject; +public: + // No inv and no bases so contracts optional if no pre, post, and override. + + /* Creation */ + + observer() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::constructor(this); + } + + virtual ~observer() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Commands */ + + // If up-to-date with related subject. + virtual bool up_to_date_with_subject(boost::contract::virtual_* v = 0) + const = 0; + + // Update this observer. + virtual void update(boost::contract::virtual_* v = 0) = 0; +}; + +bool observer::up_to_date_with_subject(boost::contract::virtual_* v) const { + boost::contract::check c = boost::contract::public_function(v, this); + assert(false); + return false; +} + +void observer::update(boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(up_to_date_with_subject()); // Up-to-date. + }) + ; + assert(false); +} + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/observer/subject.hpp b/src/boost/libs/contract/example/mitchell02/observer/subject.hpp new file mode 100644 index 000000000..12aeae71b --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/observer/subject.hpp @@ -0,0 +1,165 @@ + +// 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 + +//[mitchell02_subject +#ifndef SUBJECT_HPP_ +#define SUBJECT_HPP_ + +#include "observer.hpp" +#include <boost/contract.hpp> +#include <vector> +#include <algorithm> +#include <cassert> + +// Subject for observer design pattern. +class subject { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT_AUDIT(all_observers_valid(observers())); // Valid. + } + +public: + /* Creation */ + + // Construct subject with no observer. + subject() { + // Check invariant. + boost::contract::check c = boost::contract::constructor(this); + } + + // Destroy subject. + virtual ~subject() { + // Check invariant. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Queries */ + + // If given object is attached. + bool attached(observer const* ob) const { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(ob); // Not null. + }) + ; + + return std::find(observers_.cbegin(), observers_.cend(), ob) != + observers_.cend(); + } + + /* Commands */ + + // Attach given object as an observer. + void attach(observer* ob) { + boost::contract::old_ptr<std::vector<observer const*> > old_observers; + #ifdef BOOST_CONTRACT_AUDITS + old_observers = BOOST_CONTRACT_OLDOF(observers()); + #endif + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(ob); // Not null. + BOOST_CONTRACT_ASSERT(!attached(ob)); // Not already attached. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(attached(ob)); // Attached. + // Others not changed (frame rule). + BOOST_CONTRACT_ASSERT_AUDIT(other_observers_unchanged( + *old_observers, observers(), ob)); + }) + ; + + observers_.push_back(ob); + } + +protected: + // Contracts could have been omitted for protected/private with no pre/post. + + /* Queries */ + + // All observers attached to this subject. + std::vector<observer const*> observers() const { + std::vector<observer const*> obs; + for(std::vector<observer*>::const_iterator i = observers_.cbegin(); + i != observers_.cend(); ++i) { + obs.push_back(*i); + } + return obs; + } + + /* Commands */ + + // Update all attached observers. + void notify() { + // Protected members use `function` (no inv and no subcontracting). + boost::contract::check c = boost::contract::function() + .postcondition([&] { + // All updated. + BOOST_CONTRACT_ASSERT_AUDIT(all_observers_updated(observers())); + }) + ; + + for(std::vector<observer*>::iterator i = observers_.begin(); + i != observers_.end(); ++i) { + // Class invariants ensure no null pointers in observers but class + // invariants not checked for non-public functions so assert here. + assert(*i); // Pointer not null (defensive programming). + (*i)->update(); + } + } + +private: + /* Contract Helpers */ + + static bool all_observers_valid(std::vector<observer const*> const& obs) { + for(std::vector<observer const*>::const_iterator i = obs.cbegin(); + i != obs.cend(); ++i) { + if(!*i) return false; + } + return true; + } + + static bool other_observers_unchanged( + std::vector<observer const*> const& old_obs, + std::vector<observer const*> const& new_obs, + observer const* ob + ) { + // Private members use `function` (no inv and no subcontracting). + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(ob); // Not null. + }) + ; + + std::vector<observer const*> remaining = new_obs; + std::remove(remaining.begin(), remaining.end(), ob); + + std::vector<observer const*>::const_iterator remaining_it = + remaining.begin(); + std::vector<observer const*>::const_iterator old_it = old_obs.begin(); + while(remaining.cend() != remaining_it && old_obs.cend() != old_it) { + if(*remaining_it != *old_it) return false; + ++remaining_it; + ++old_it; + } + return true; + } + + static bool all_observers_updated(std::vector<observer const*> const& obs) { + for(std::vector<observer const*>::const_iterator i = obs.cbegin(); + i != obs.cend(); ++i) { + if(!*i) return false; + if(!(*i)->up_to_date_with_subject()) return false; + } + return true; + } + + std::vector<observer*> observers_; +}; + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/observer_main.cpp b/src/boost/libs/contract/example/mitchell02/observer_main.cpp new file mode 100644 index 000000000..0f6c1a5b8 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/observer_main.cpp @@ -0,0 +1,118 @@ + +// 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 + +//[mitchell02_observer_main +#include "observer/observer.hpp" +#include "observer/subject.hpp" +#include <boost/contract.hpp> +#include <cassert> + +int test_state; // For testing only. + +// Implement an actual subject. +class concrete_subject + #define BASES public subject + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. + #undef BASES + +public: + typedef int state; // Some state being observed. + + concrete_subject() : state_() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::constructor(this); + } + + virtual ~concrete_subject() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + void set_state(state const& new_state) { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::public_function(this); + + state_ = new_state; + assert(state_ == test_state); + notify(); // Notify all observers. + } + + state get_state() const { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::public_function(this); + return state_; + } + +private: + state state_; +}; + +// Implement an actual observer. +class concrete_observer + #define BASES public observer + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. + #undef BASES + + BOOST_CONTRACT_OVERRIDES(up_to_date_with_subject, update) + +public: + // Create concrete observer. + explicit concrete_observer(concrete_subject const& subj) : + subject_(subj), observed_state_() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::constructor(this); + } + + virtual ~concrete_observer() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + // Implement base virtual functions. + + bool up_to_date_with_subject(boost::contract::virtual_* v = 0) + const /* override */ { + bool result; + boost::contract::check c = boost::contract::public_function< + override_up_to_date_with_subject + >(v, result, &concrete_observer::up_to_date_with_subject, this); + + return result = true; // For simplicity, assume always up-to-date. + } + + void update(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_update>(v, &concrete_observer::update, this); + + observed_state_ = subject_.get_state(); + assert(observed_state_ == test_state); + } + +private: + concrete_subject const& subject_; + concrete_subject::state observed_state_; +}; + +int main() { + concrete_subject subj; + concrete_observer ob(subj); + subj.attach(&ob); + + subj.set_state(test_state = 123); + subj.set_state(test_state = 456); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/simple_queue.cpp b/src/boost/libs/contract/example/mitchell02/simple_queue.cpp new file mode 100644 index 000000000..e0250137f --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/simple_queue.cpp @@ -0,0 +1,219 @@ + +// 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 + +//[mitchell02_simple_queue +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <vector> +#include <cassert> + +template<typename T> +class simple_queue + #define BASES private boost::contract::constructor_precondition< \ + simple_queue<T> > + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + void invariant() const { + BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. + } + +public: + /* Creation */ + + // Create empty queue. + explicit simple_queue(int a_capacity) : + boost::contract::constructor_precondition<simple_queue>([&] { + BOOST_CONTRACT_ASSERT(a_capacity > 0); // Positive capacity. + }) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + // Capacity set. + BOOST_CONTRACT_ASSERT(capacity() == a_capacity); + BOOST_CONTRACT_ASSERT(is_empty()); // Empty. + }) + ; + + items_.reserve(a_capacity); + } + + // Destroy queue. + virtual ~simple_queue() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Basic Queries */ + + // Items in queue (in their order). + // (Somewhat exposes implementation but allows to check more contracts.) + std::vector<T> const& items() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return items_; + } + + // Max number of items queue can hold. + int capacity() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return items_.capacity(); + } + + /* Derived Queries */ + + // Number of items. + int count() const { + int result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Return items count. + BOOST_CONTRACT_ASSERT(result == int(items().size())); + }) + ; + + return result = items_.size(); + } + + // Item at head. + T const& head() const { + boost::optional<T const&> result; + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!is_empty()); // Not empty. + }) + .postcondition([&] { + // Return item on top. + BOOST_CONTRACT_ASSERT(*result == items().at(0)); + }) + ; + + return *(result = items_.at(0)); + } + + // If queue contains no item. + bool is_empty() const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Consistent with count. + BOOST_CONTRACT_ASSERT(result == (count() == 0)); + }) + ; + + return result = (items_.size() == 0); + } + + // If queue has no room for another item. + bool is_full() const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT( // Consistent with size and capacity. + result == (capacity() == int(items().size()))); + }) + ; + + return result = (items_.size() == items_.capacity()); + } + + /* Commands */ + + // Remove head itme and shift all other items. + void remove() { + // Expensive all_equal postcond. and old_items copy might be skipped. + boost::contract::old_ptr<std::vector<T> > old_items; + #ifdef BOOST_CONTRACT_AUDIITS + = BOOST_CONTRACT_OLDOF(items()) + #endif // Else, leave old pointer null... + ; + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!is_empty()); // Not empty. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec. + // ...following skipped #ifndef AUDITS. + if(old_items) all_equal(items(), *old_items, /* shifted = */ 1); + }) + ; + + items_.erase(items_.begin()); + } + + // Add item to tail. + void put(T const& item) { + // Expensive all_equal postcond. and old_items copy might be skipped. + boost::contract::old_ptr<std::vector<T> > old_items; + #ifdef BOOST_CONTRACT_AUDITS + = BOOST_CONTRACT_OLDOF(items()) + #endif // Else, leave old pointer null... + ; + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(count() < capacity()); // Room for add. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc. + // Second to last item. + BOOST_CONTRACT_ASSERT(items().at(count() - 1) == item); + // ...following skipped #ifndef AUDITS. + if(old_items) all_equal(items(), *old_items); + }) + ; + + items_.push_back(item); + } + +private: + // Contract helper. + static bool all_equal(std::vector<T> const& left, + std::vector<T> const& right, unsigned offset = 0) { + boost::contract::check c = boost::contract::function() + .precondition([&] { + // Correct offset. + BOOST_CONTRACT_ASSERT(right.size() == left.size() + offset); + }) + ; + + for(unsigned i = offset; i < right.size(); ++i) { + if(left.at(i - offset) != right.at(i)) return false; + } + return true; + } + + std::vector<T> items_; +}; + +int main() { + simple_queue<int> q(10); + q.put(123); + q.put(456); + + assert(q.capacity() == 10); + assert(q.head() == 123); + + assert(!q.is_empty()); + assert(!q.is_full()); + + std::vector<int> const& items = q.items(); + assert(items.at(0) == 123); + assert(items.at(1) == 456); + + q.remove(); + assert(q.count() == 1); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/stack.cpp b/src/boost/libs/contract/example/mitchell02/stack.cpp new file mode 100644 index 000000000..a0bd6b144 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/stack.cpp @@ -0,0 +1,138 @@ + +// 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 + +//[mitchell02_stack +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <vector> +#include <cassert> + +template<typename T> +class stack { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. + } + +public: + /* Creation */ + + // Create empty stack. + stack() { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == 0); // Empty. + }) + ; + } + + // Destroy stack. + virtual ~stack() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Basic Queries */ + + // Number of items. + int count() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return items_.size(); + } + + // Item at index in [1, count()] (as in Eiffel). + T const& item_at(int index) const { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(index > 0); // Positive index. + BOOST_CONTRACT_ASSERT(index <= count()); // Index within count. + }) + ; + + return items_[index - 1]; + } + + /* Derived Queries */ + + // If no items. + bool is_empty() const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Consistent with count. + BOOST_CONTRACT_ASSERT(result == (count() == 0)); + }) + ; + + return result = (count() == 0); + } + + // Top item. + T const& item() const { + boost::optional<T const&> result; // Avoid extra construction of T. + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(count() > 0); // Not empty. + }) + .postcondition([&] { + // Item on top. + BOOST_CONTRACT_ASSERT(*result == item_at(count())); + }) + ; + + return *(result = item_at(count())); + } + + /* Commands */ + + // Push item to the top. + void put(T const& new_item) { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc. + BOOST_CONTRACT_ASSERT(item() == new_item); // Item set. + }) + ; + + items_.push_back(new_item); + } + + // Pop top item. + void remove() { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(count() > 0); // Not empty. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec. + }) + ; + + items_.pop_back(); + } + +private: + std::vector<T> items_; +}; + +int main() { + stack<int> s; + assert(s.count() == 0); + + s.put(123); + assert(s.item() == 123); + + s.remove(); + assert(s.is_empty()); + + return 0; +} +//] + 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. +//] + |