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