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 #include <boost/contract.hpp>
8 #include <vector>
9 #include <algorithm>
10 #include <cassert>
11
12 template<typename T>
13 class pushable {
14 public:
invariant() const15 void invariant() const {
16 BOOST_CONTRACT_ASSERT(capacity() <= max_size());
17 }
18
19 virtual void push_back(T x, boost::contract::virtual_* v = 0) = 0;
20
21 protected:
22 virtual unsigned capacity() const = 0;
23 virtual unsigned max_size() const = 0;
24 };
25
26 template<typename T>
push_back(T x,boost::contract::virtual_ * v)27 void pushable<T>::push_back(T x, boost::contract::virtual_* v) {
28 boost::contract::old_ptr<unsigned> old_capacity =
29 BOOST_CONTRACT_OLDOF(v, capacity());
30 boost::contract::check c = boost::contract::public_function(v, this)
31 .precondition([&] {
32 BOOST_CONTRACT_ASSERT(capacity() < max_size());
33 })
34 .postcondition([&] {
35 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
36 })
37 ;
38 assert(false); // Shall never execute this body.
39 }
40
41 struct has_size { virtual unsigned size() const = 0; };
42 struct has_empty { virtual bool empty() const = 0; };
43
44 class unique_chars
45 : private boost::contract::constructor_precondition<unique_chars>
46 {
47 public:
invariant() const48 void invariant() const {
49 BOOST_CONTRACT_ASSERT(size() >= 0);
50 }
51
unique_chars(char from,char to)52 unique_chars(char from, char to) :
53 boost::contract::constructor_precondition<unique_chars>([&] {
54 BOOST_CONTRACT_ASSERT(from <= to);
55 })
56 {
57 boost::contract::check c = boost::contract::constructor(this)
__anon88752e880402null58 .postcondition([&] {
59 BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1));
60 })
61 ;
62
63 for(char x = from; x <= to; ++x) vect_.push_back(x);
64 }
65
~unique_chars()66 virtual ~unique_chars() {
67 boost::contract::check c = boost::contract::destructor(this);
68 }
69
size() const70 unsigned size() const {
71 boost::contract::check c = boost::contract::public_function(this);
72 return vect_.size();
73 }
74
find(char x) const75 bool find(char x) const {
76 bool result;
77 boost::contract::check c = boost::contract::public_function(this)
78 .postcondition([&] {
79 if(size() == 0) BOOST_CONTRACT_ASSERT(!result);
80 })
81 ;
82
83 return result = std::find(vect_.begin(), vect_.end(), x) != vect_.end();
84 }
85
push_back(char x,boost::contract::virtual_ * v=0)86 virtual void push_back(char x, boost::contract::virtual_* v = 0) {
87 boost::contract::old_ptr<bool> old_find =
88 BOOST_CONTRACT_OLDOF(v, find(x));
89 boost::contract::old_ptr<unsigned> old_size =
90 BOOST_CONTRACT_OLDOF(v, size());
91 boost::contract::check c = boost::contract::public_function(v, this)
92 .precondition([&] {
93 BOOST_CONTRACT_ASSERT(!find(x));
94 })
95 .postcondition([&] {
96 if(!*old_find) {
97 BOOST_CONTRACT_ASSERT(find(x));
98 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
99 }
100 })
101 ;
102
103 vect_.push_back(x);
104 }
105
106 protected:
unique_chars()107 unique_chars() {}
108
vect() const109 std::vector<char> const& vect() const { return vect_; }
110
111 private:
112 std::vector<char> vect_;
113 };
114
115 //[base_types
116 class chars
117 #define BASES /* local macro (for convenience) */ \
118 private boost::contract::constructor_precondition<chars>, \
119 public unique_chars, \
120 public virtual pushable<char>, \
121 virtual protected has_size, \
122 private has_empty
123 : BASES // Bases of this class.
124 {
125 public:
126 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Bases typedef.
127 #undef BASES // Undefine local macro.
128
129 /* ... */
130 //]
131
invariant() const132 void invariant() const {
133 BOOST_CONTRACT_ASSERT(empty() == (size() == 0));
134 }
135
chars(char from,char to)136 chars(char from, char to) : unique_chars(from, to) {
137 boost::contract::check c = boost::contract::constructor(this);
138 }
139
chars(char const * const c_str)140 chars(char const* const c_str) :
141 boost::contract::constructor_precondition<chars>([&] {
142 BOOST_CONTRACT_ASSERT(c_str[0] != '\0');
143 })
144 {
145 boost::contract::check c = boost::contract::constructor(this);
146
147 for(unsigned i = 0; c_str[i] != '\0'; ++i) push_back(c_str[i]);
148 }
149
push_back(char x,boost::contract::virtual_ * v=0)150 void push_back(char x, boost::contract::virtual_* v = 0) /* override */ {
151 boost::contract::old_ptr<bool> old_find =
152 BOOST_CONTRACT_OLDOF(v, find(x));
153 boost::contract::old_ptr<unsigned> old_size =
154 BOOST_CONTRACT_OLDOF(v, size());
155 boost::contract::check c = boost::contract::public_function<
156 override_push_back>(v, &chars::push_back, this, x)
157 .precondition([&] {
158 BOOST_CONTRACT_ASSERT(find(x));
159 })
160 .postcondition([&] {
161 if(*old_find) BOOST_CONTRACT_ASSERT(size() == *old_size);
162 })
163 ;
164
165 if(!find(x)) unique_chars::push_back(x);
166 }
167 BOOST_CONTRACT_OVERRIDE(push_back);
168
empty() const169 bool empty() const {
170 boost::contract::check c = boost::contract::public_function(this);
171 return size() == 0;
172 }
173
size() const174 unsigned size() const { return unique_chars::size(); }
175
176 protected:
max_size() const177 unsigned max_size() const { return vect().max_size(); }
capacity() const178 unsigned capacity() const { return vect().capacity(); }
179 };
180
main()181 int main() {
182 chars s("abc");
183 assert(s.find('a'));
184 assert(s.find('b'));
185 assert(!s.find('x'));
186 return 0;
187 }
188
189