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