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 //[meyer97_stack3
8 // File: stack3.cpp
9 #include "stack4.hpp"
10 #include <boost/contract.hpp>
11 #include <boost/optional.hpp>
12 #include <cassert>
13
14 // Dispenser LIFO with max capacity using error codes.
15 template<typename T>
16 class stack3 {
17 friend class boost::contract::access;
18
invariant() const19 void invariant() const {
20 if(!error()) {
21 BOOST_CONTRACT_ASSERT(count() >= 0); // Count non-negative.
22 BOOST_CONTRACT_ASSERT(count() <= capacity()); // Count bounded.
23 // Empty if no element.
24 BOOST_CONTRACT_ASSERT(empty() == (count() == 0));
25 }
26 }
27
28 public:
29 enum error_code {
30 no_error = 0,
31 overflow_error,
32 underflow_error,
33 size_error
34 };
35
36 /* Initialization */
37
38 // Create stack for max of n elems, if n < 0 set error (no preconditions).
stack3(int n,T const & default_value=T ())39 explicit stack3(int n, T const& default_value = T()) :
40 stack_(0), error_(no_error) {
41 boost::contract::check c = boost::contract::constructor(this)
42 .postcondition([&] {
43 // Error if impossible.
44 BOOST_CONTRACT_ASSERT((n < 0) == (error() == size_error));
45 // No error if possible.
46 BOOST_CONTRACT_ASSERT((n >= 0) == !error());
47 // Created if no error.
48 if(!error()) BOOST_CONTRACT_ASSERT(capacity() == n);
49 })
50 ;
51
52 if(n >= 0) stack_ = stack4<T>(n);
53 else error_ = size_error;
54 }
55
56 /* Access */
57
58 // Max number of stack elements.
capacity() const59 int capacity() const {
60 // Check invariants.
61 boost::contract::check c = boost::contract::public_function(this);
62 return stack_.capacity();
63 }
64
65 // Number of stack elements.
count() const66 int count() const {
67 // Check invariants.
68 boost::contract::check c = boost::contract::public_function(this);
69 return stack_.count();
70 }
71
72 // Top element if present, otherwise none and set error (no preconditions).
item() const73 boost::optional<T const&> item() const {
74 boost::contract::check c = boost::contract::public_function(this)
75 .postcondition([&] {
76 // Error if impossible.
77 BOOST_CONTRACT_ASSERT(empty() == (error() == underflow_error));
78 // No error if possible.
79 BOOST_CONTRACT_ASSERT(!empty() == !error());
80 })
81 ;
82
83 if(!empty()) {
84 error_ = no_error;
85 return boost::optional<T const&>(stack_.item());
86 } else {
87 error_ = underflow_error;
88 return boost::optional<T const&>();
89 }
90 }
91
92 /* Status Report */
93
94 // Error indicator set by various operations.
error() const95 error_code error() const {
96 // Check invariants.
97 boost::contract::check c = boost::contract::public_function(this);
98 return error_;
99 }
100
empty() const101 bool empty() const {
102 // Check invariants.
103 boost::contract::check c = boost::contract::public_function(this);
104 return stack_.empty();
105 }
106
full() const107 bool full() const {
108 // Check invariants.
109 boost::contract::check c = boost::contract::public_function(this);
110 return stack_.full();
111 }
112
113 /* Element Change */
114
115 // Add x to top if capacity allows, otherwise set error (no preconditions).
put(T const & x)116 void put(T const& x) {
117 boost::contract::old_ptr<bool> old_full = BOOST_CONTRACT_OLDOF(full());
118 boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
119 boost::contract::check c = boost::contract::public_function(this)
120 .postcondition([&] {
121 // Error if impossible.
122 BOOST_CONTRACT_ASSERT(*old_full == (error() == overflow_error));
123 // No error if possible.
124 BOOST_CONTRACT_ASSERT(!*old_full == !error());
125 if(!error()) { // If no error...
126 BOOST_CONTRACT_ASSERT(!empty()); // ...not empty.
127 BOOST_CONTRACT_ASSERT(*item() == x); // ...added to top.
128 // ...one more.
129 BOOST_CONTRACT_ASSERT(count() == *old_count + 1);
130 }
131 })
132 ;
133
134 if(full()) error_ = overflow_error;
135 else {
136 stack_.put(x);
137 error_ = no_error;
138 }
139 }
140
141 // Remove top element if possible, otherwise set error (no preconditions).
remove()142 void remove() {
143 boost::contract::old_ptr<bool> old_empty =
144 BOOST_CONTRACT_OLDOF(empty());
145 boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
146 boost::contract::check c = boost::contract::public_function(this)
147 .postcondition([&] {
148 // Error if impossible.
149 BOOST_CONTRACT_ASSERT(*old_empty == (error() ==
150 underflow_error));
151 // No error if possible.
152 BOOST_CONTRACT_ASSERT(!*old_empty == !error());
153 if(!error()) { // If no error...
154 BOOST_CONTRACT_ASSERT(!full()); // ...not full.
155 // ...one less.
156 BOOST_CONTRACT_ASSERT(count() == *old_count - 1);
157 }
158 })
159 ;
160
161 if(empty()) error_ = underflow_error;
162 else {
163 stack_.remove();
164 error_ = no_error;
165 }
166 }
167
168 private:
169 stack4<T> stack_;
170 mutable error_code error_;
171 };
172
main()173 int main() {
174 stack3<int> s(3);
175 assert(s.capacity() == 3);
176 assert(s.count() == 0);
177 assert(s.empty());
178 assert(!s.full());
179
180 s.put(123);
181 assert(!s.empty());
182 assert(!s.full());
183 assert(*s.item() == 123);
184
185 s.remove();
186 assert(s.empty());
187 assert(!s.full());
188
189 return 0;
190 }
191 //]
192
193