diff options
Diffstat (limited to 'src/boost/libs/contract/example/meyer97/stack3.cpp')
| -rw-r--r-- | src/boost/libs/contract/example/meyer97/stack3.cpp | 192 |
1 files changed, 192 insertions, 0 deletions
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; +} +//] + |