1 2 // Copyright (C) 2008-2018 Lorenzo Caminiti 3 // Distributed under the Boost Software License, Version 1.0 (see accompanying 4 // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt). 5 // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html 6 7 //[cline90_stack 8 #include <boost/contract.hpp> 9 #include <cassert> 10 11 // NOTE: Incomplete contract assertions, addressing only `empty` and `full`. 12 template<typename T> 13 class stack 14 #define BASES private boost::contract::constructor_precondition<stack<T> > 15 : BASES 16 { 17 friend class boost::contract::access; 18 19 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; 20 #undef BASES 21 22 public: stack(int capacity)23 explicit stack(int capacity) : 24 boost::contract::constructor_precondition<stack>([&] { 25 BOOST_CONTRACT_ASSERT(capacity >= 0); 26 }), 27 data_(new T[capacity]), capacity_(capacity), size_(0) 28 { 29 boost::contract::check c = boost::contract::constructor(this) __anon552217250202null30 .postcondition([&] { 31 BOOST_CONTRACT_ASSERT(empty()); 32 BOOST_CONTRACT_ASSERT(full() == (capacity == 0)); 33 }) 34 ; 35 36 for(int i = 0; i < capacity_; ++i) data_[i] = T(); 37 } 38 ~stack()39 virtual ~stack() { 40 boost::contract::check c = boost::contract::destructor(this); 41 delete[] data_; 42 } 43 empty() const44 bool empty() const { 45 boost::contract::check c = boost::contract::public_function(this); 46 return size_ == 0; 47 } 48 full() const49 bool full() const { 50 boost::contract::check c = boost::contract::public_function(this); 51 return size_ == capacity_; 52 } 53 push(T const & value)54 void push(T const& value) { 55 boost::contract::check c = boost::contract::public_function(this) 56 .precondition([&] { 57 BOOST_CONTRACT_ASSERT(!full()); 58 }) 59 .postcondition([&] { 60 BOOST_CONTRACT_ASSERT(!empty()); 61 }) 62 ; 63 64 data_[size_++] = value; 65 } 66 pop()67 T pop() { 68 boost::contract::check c = boost::contract::public_function(this) 69 .precondition([&] { 70 BOOST_CONTRACT_ASSERT(!empty()); 71 }) 72 .postcondition([&] { 73 BOOST_CONTRACT_ASSERT(!full()); 74 }) 75 ; 76 77 return data_[--size_]; 78 } 79 80 private: 81 T* data_; 82 int capacity_; 83 int size_; 84 }; 85 main()86int main() { 87 stack<int> s(3); 88 s.push(123); 89 assert(s.pop() == 123); 90 return 0; 91 } 92 //] 93 94