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
12template<typename T>
13class pushable {
14public:
15 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
21protected:
22 virtual unsigned capacity() const = 0;
23 virtual unsigned max_size() const = 0;
24};
25
26template<typename T>
27void 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
41struct has_size { virtual unsigned size() const = 0; };
42struct has_empty { virtual bool empty() const = 0; };
43
44class unique_chars
45 : private boost::contract::constructor_precondition<unique_chars>
46{
47public:
48 void invariant() const {
49 BOOST_CONTRACT_ASSERT(size() >= 0);
50 }
51
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(obj: this)
58 .postcondition(f: [&] {
59 BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1));
60 })
61 ;
62
63 for(char x = from; x <= to; ++x) vect_.push_back(x: x);
64 }
65
66 virtual ~unique_chars() {
67 boost::contract::check c = boost::contract::destructor(obj: this);
68 }
69
70 unsigned size() const {
71 boost::contract::check c = boost::contract::public_function(obj: this);
72 return vect_.size();
73 }
74
75 bool find(char x) const {
76 bool result;
77 boost::contract::check c = boost::contract::public_function(obj: this)
78 .postcondition(f: [&] {
79 if(size() == 0) BOOST_CONTRACT_ASSERT(!result);
80 })
81 ;
82
83 return result = std::find(first: vect_.begin(), last: vect_.end(), val: x) != vect_.end();
84 }
85
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, obj: this)
92 .precondition(f: [&] {
93 BOOST_CONTRACT_ASSERT(!find(x));
94 })
95 .postcondition(f: [&] {
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: x);
104 }
105
106protected:
107 unique_chars() {}
108
109 std::vector<char> const& vect() const { return vect_; }
110
111private:
112 std::vector<char> vect_;
113};
114
115//[base_types
116class 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{
125public:
126 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Bases typedef.
127 #undef BASES // Undefine local macro.
128
129 /* ... */
130//]
131
132 void invariant() const {
133 BOOST_CONTRACT_ASSERT(empty() == (size() == 0));
134 }
135
136 chars(char from, char to) : unique_chars(from, to) {
137 boost::contract::check c = boost::contract::constructor(obj: this);
138 }
139
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(obj: this);
146
147 for(unsigned i = 0; c_str[i] != '\0'; ++i) push_back(x: c_str[i]);
148 }
149
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, obj: this, args&: x)
157 .precondition(f: [&] {
158 BOOST_CONTRACT_ASSERT(find(x));
159 })
160 .postcondition(f: [&] {
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
169 bool empty() const {
170 boost::contract::check c = boost::contract::public_function(obj: this);
171 return size() == 0;
172 }
173
174 unsigned size() const { return unique_chars::size(); }
175
176protected:
177 unsigned max_size() const { return vect().max_size(); }
178 unsigned capacity() const { return vect().capacity(); }
179};
180
181int 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

source code of boost/libs/contract/example/features/base_types.cpp