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 //[mitchell02_stack 8 #include <boost/contract.hpp> 9 #include <boost/optional.hpp> 10 #include <vector> 11 #include <cassert> 12 13 template<typename T> 14 class stack { 15 friend class boost::contract::access; 16 invariant() const17 void invariant() const { 18 BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. 19 } 20 21 public: 22 /* Creation */ 23 24 // Create empty stack. stack()25 stack() { 26 boost::contract::check c = boost::contract::constructor(this) 27 .postcondition([&] { 28 BOOST_CONTRACT_ASSERT(count() == 0); // Empty. 29 }) 30 ; 31 } 32 33 // Destroy stack. ~stack()34 virtual ~stack() { 35 // Check invariants. 36 boost::contract::check c = boost::contract::destructor(this); 37 } 38 39 /* Basic Queries */ 40 41 // Number of items. count() const42 int count() const { 43 // Check invariants. 44 boost::contract::check c = boost::contract::public_function(this); 45 return items_.size(); 46 } 47 48 // Item at index in [1, count()] (as in Eiffel). item_at(int index) const49 T const& item_at(int index) const { 50 boost::contract::check c = boost::contract::public_function(this) 51 .precondition([&] { 52 BOOST_CONTRACT_ASSERT(index > 0); // Positive index. 53 BOOST_CONTRACT_ASSERT(index <= count()); // Index within count. 54 }) 55 ; 56 57 return items_[index - 1]; 58 } 59 60 /* Derived Queries */ 61 62 // If no items. is_empty() const63 bool is_empty() const { 64 bool result; 65 boost::contract::check c = boost::contract::public_function(this) 66 .postcondition([&] { 67 // Consistent with count. 68 BOOST_CONTRACT_ASSERT(result == (count() == 0)); 69 }) 70 ; 71 72 return result = (count() == 0); 73 } 74 75 // Top item. item() const76 T const& item() const { 77 boost::optional<T const&> result; // Avoid extra construction of T. 78 boost::contract::check c = boost::contract::public_function(this) 79 .precondition([&] { 80 BOOST_CONTRACT_ASSERT(count() > 0); // Not empty. 81 }) 82 .postcondition([&] { 83 // Item on top. 84 BOOST_CONTRACT_ASSERT(*result == item_at(count())); 85 }) 86 ; 87 88 return *(result = item_at(count())); 89 } 90 91 /* Commands */ 92 93 // Push item to the top. put(T const & new_item)94 void put(T const& new_item) { 95 boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); 96 boost::contract::check c = boost::contract::public_function(this) 97 .postcondition([&] { 98 BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc. 99 BOOST_CONTRACT_ASSERT(item() == new_item); // Item set. 100 }) 101 ; 102 103 items_.push_back(new_item); 104 } 105 106 // Pop top item. remove()107 void remove() { 108 boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); 109 boost::contract::check c = boost::contract::public_function(this) 110 .precondition([&] { 111 BOOST_CONTRACT_ASSERT(count() > 0); // Not empty. 112 }) 113 .postcondition([&] { 114 BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec. 115 }) 116 ; 117 118 items_.pop_back(); 119 } 120 121 private: 122 std::vector<T> items_; 123 }; 124 main()125int main() { 126 stack<int> s; 127 assert(s.count() == 0); 128 129 s.put(123); 130 assert(s.item() == 123); 131 132 s.remove(); 133 assert(s.is_empty()); 134 135 return 0; 136 } 137 //] 138 139