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_vstack
8 #include "vector.hpp"
9 #include <boost/contract.hpp>
10 #include <boost/optional.hpp>
11 #include <cassert>
12
13 // NOTE: Incomplete contract assertions, addressing only `empty` and `full`.
14 template<typename T>
15 class abstract_stack {
16 public:
abstract_stack()17 abstract_stack() {
18 boost::contract::check c = boost::contract::constructor(this)
19 .postcondition([&] {
20 // AXIOM as empty() cannot actually be checked here to avoid
21 // calling pure virtual function length() during construction).
22 BOOST_CONTRACT_ASSERT_AXIOM(empty());
23 })
24 ;
25 }
26
~abstract_stack()27 virtual ~abstract_stack() {
28 boost::contract::check c = boost::contract::destructor(this);
29 }
30
full() const31 bool full() const {
32 bool result;
33 boost::contract::check c = boost::contract::public_function(this)
34 .postcondition([&] {
35 BOOST_CONTRACT_ASSERT(result == (length() == capacity()));
36 })
37 ;
38
39 return result = (length() == capacity());
40 }
41
empty() const42 bool empty() const {
43 bool result;
44 boost::contract::check c = boost::contract::public_function(this)
45 .postcondition([&] {
46 BOOST_CONTRACT_ASSERT(result = (length() == 0));
47 })
48 ;
49
50 return result = (length() == 0);
51 }
52
53 virtual int length(boost::contract::virtual_* v = 0) const = 0;
54 virtual int capacity(boost::contract::virtual_* v = 0) const = 0;
55
56 virtual T const& item(boost::contract::virtual_* v = 0) const = 0;
57
58 virtual void push(T const& value, boost::contract::virtual_* v = 0) = 0;
59 virtual T const& pop(boost::contract::virtual_* v = 0) = 0;
60
61 virtual void clear(boost::contract::virtual_* v = 0) = 0;
62 };
63
64 template<typename T>
length(boost::contract::virtual_ * v) const65 int abstract_stack<T>::length(boost::contract::virtual_* v) const {
66 int result;
67 boost::contract::check c = boost::contract::public_function(v, result, this)
68 .postcondition([&] (int const& result) {
69 BOOST_CONTRACT_ASSERT(result >= 0);
70 })
71 ;
72 assert(false);
73 return result;
74 }
75
76 template<typename T>
capacity(boost::contract::virtual_ * v) const77 int abstract_stack<T>::capacity(boost::contract::virtual_* v) const {
78 int result;
79 boost::contract::check c = boost::contract::public_function(v, result, this)
80 .postcondition([&] (int const& result) {
81 BOOST_CONTRACT_ASSERT(result >= 0);
82 })
83 ;
84 assert(false);
85 return result;
86 }
87
88 template<typename T>
item(boost::contract::virtual_ * v) const89 T const& abstract_stack<T>::item(boost::contract::virtual_* v) const {
90 boost::optional<T const&> result;
91 boost::contract::check c = boost::contract::public_function(v, result, this)
92 .precondition([&] {
93 BOOST_CONTRACT_ASSERT(!empty());
94 })
95 ;
96 assert(false);
97 return *result;
98 }
99
100 template<typename T>
push(T const & value,boost::contract::virtual_ * v)101 void abstract_stack<T>::push(T const& value, boost::contract::virtual_* v) {
102 boost::contract::check c = boost::contract::public_function(v, this)
103 .precondition([&] {
104 BOOST_CONTRACT_ASSERT(!full());
105 })
106 .postcondition([&] {
107 BOOST_CONTRACT_ASSERT(!empty());
108 })
109 ;
110 assert(false);
111 }
112
113 template<typename T>
pop(boost::contract::virtual_ * v)114 T const& abstract_stack<T>::pop(boost::contract::virtual_* v) {
115 boost::optional<T const&> result;
116 boost::contract::old_ptr<T> old_item = BOOST_CONTRACT_OLDOF(v, item());
117 boost::contract::check c = boost::contract::public_function(v, result, this)
118 .precondition([&] {
119 BOOST_CONTRACT_ASSERT(!empty());
120 })
121 .postcondition([&] (boost::optional<T const&> const& result) {
122 BOOST_CONTRACT_ASSERT(!full());
123 BOOST_CONTRACT_ASSERT(*result == *old_item);
124 })
125 ;
126 assert(false);
127 return *result;
128 }
129
130 template<typename T>
clear(boost::contract::virtual_ * v)131 void abstract_stack<T>::clear(boost::contract::virtual_* v) {
132 boost::contract::check c = boost::contract::public_function(v, this)
133 .postcondition([&] {
134 BOOST_CONTRACT_ASSERT(empty());
135 })
136 ;
137 assert(false);
138 }
139
140 template<typename T>
141 class vstack
142 #define BASES private boost::contract::constructor_precondition< \
143 vstack<T> >, public abstract_stack<T>
144 : BASES
145 {
146 friend class boost::contract::access;
147
148 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
149 #undef BASES
150
invariant() const151 void invariant() const {
152 BOOST_CONTRACT_ASSERT(length() >= 0);
153 BOOST_CONTRACT_ASSERT(length() < capacity());
154 }
155
156 BOOST_CONTRACT_OVERRIDES(length, capacity, item, push, pop, clear)
157
158 public:
vstack(int count=10)159 explicit vstack(int count = 10) :
160 boost::contract::constructor_precondition<vstack>([&] {
161 BOOST_CONTRACT_ASSERT(count >= 0);
162 }),
163 vect_(count), // OK, executed after precondition so count >= 0.
164 len_(0)
165 {
166 boost::contract::check c = boost::contract::constructor(this)
__anon92ccc7ba0d02null167 .postcondition([&] {
168 BOOST_CONTRACT_ASSERT(length() == 0);
169 BOOST_CONTRACT_ASSERT(capacity() == count);
170 })
171 ;
172 }
173
~vstack()174 virtual ~vstack() {
175 boost::contract::check c = boost::contract::destructor(this);
176 }
177
178 // Inherited from abstract_stack.
179
length(boost::contract::virtual_ * v=0) const180 virtual int length(boost::contract::virtual_* v = 0) const /* override */ {
181 int result;
182 boost::contract::check c = boost::contract::public_function<
183 override_length>(v, result, &vstack::length, this);
184 return result = len_;
185 }
186
capacity(boost::contract::virtual_ * v=0) const187 virtual int capacity(boost::contract::virtual_* v = 0)
188 const /* override */ {
189 int result;
190 boost::contract::check c = boost::contract::public_function<
191 override_capacity>(v, result, &vstack::capacity, this);
192 return result = vect_.size();
193 }
194
item(boost::contract::virtual_ * v=0) const195 virtual T const& item(boost::contract::virtual_* v = 0)
196 const /* override */ {
197 boost::optional<T const&> result;
198 boost::contract::check c = boost::contract::public_function<
199 override_item>(v, result, &vstack::item, this);
200 return *(result = vect_[len_ - 1]);
201 }
202
push(T const & value,boost::contract::virtual_ * v=0)203 virtual void push(T const& value, boost::contract::virtual_* v = 0)
204 /* override */ {
205 boost::contract::check c = boost::contract::public_function<
206 override_push>(v, &vstack::push, this, value);
207 vect_[len_++] = value;
208 }
209
pop(boost::contract::virtual_ * v=0)210 virtual T const& pop(boost::contract::virtual_* v = 0) /* override */ {
211 boost::optional<T const&> result;
212 boost::contract::check c = boost::contract::public_function<
213 override_pop>(v, result, &vstack::pop, this);
214 return *(result = vect_[--len_]);
215 }
216
clear(boost::contract::virtual_ * v=0)217 virtual void clear(boost::contract::virtual_* v = 0) /* override */ {
218 boost::contract::check c = boost::contract::public_function<
219 override_clear>(v, &vstack::clear, this);
220 len_ = 0;
221 }
222
223 private:
224 vector<T> vect_;
225 int len_;
226 };
227
main()228 int main() {
229 vstack<int> s(3);
230 assert(s.capacity() == 3);
231
232 s.push(123);
233 assert(s.length() == 1);
234 assert(s.pop() == 123);
235
236 return 0;
237 }
238 //]
239
240