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`.
14template<typename T>
15class abstract_stack {
16public:
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
27 virtual ~abstract_stack() {
28 boost::contract::check c = boost::contract::destructor(this);
29 }
30
31 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
42 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
64template<typename T>
65int 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
76template<typename T>
77int 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
88template<typename T>
89T 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
100template<typename T>
101void 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
113template<typename T>
114T 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
130template<typename T>
131void 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
140template<typename T>
141class 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
151 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
158public:
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)
167 .postcondition([&] {
168 BOOST_CONTRACT_ASSERT(length() == 0);
169 BOOST_CONTRACT_ASSERT(capacity() == count);
170 })
171 ;
172 }
173
174 virtual ~vstack() {
175 boost::contract::check c = boost::contract::destructor(this);
176 }
177
178 // Inherited from abstract_stack.
179
180 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
187 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
195 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
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
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
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
223private:
224 vector<T> vect_;
225 int len_;
226};
227
228int main() {
229 vstack<int> s(3);
230 assert(s.capacity() == 3);
231
232 s.push(value: 123);
233 assert(s.length() == 1);
234 assert(s.pop() == 123);
235
236 return 0;
237}
238//]
239
240

source code of boost/libs/contract/example/cline90/vstack.cpp