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 <vector>
8 #include <limits>
9 #include <cassert>
10
11 //[ifdef_function
12 // Use #ifdef to completely disable contract code compilation.
13 #include <boost/contract/core/config.hpp>
14 #ifndef BOOST_CONTRACT_NO_ALL
15 #include <boost/contract.hpp>
16 #endif
17
inc(int & x)18 int inc(int& x) {
19 int result;
20 #ifndef BOOST_CONTRACT_NO_OLDS
21 boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x);
22 #endif
23 #ifndef BOOST_CONTRACT_NO_FUNCTIONS
24 boost::contract::check c = boost::contract::function()
25 #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
26 .precondition([&] {
27 BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max());
28 })
29 #endif
30 #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
31 .postcondition([&] {
32 BOOST_CONTRACT_ASSERT(x == *old_x + 1);
33 BOOST_CONTRACT_ASSERT(result == *old_x);
34 })
35 #endif
36 ;
37 #endif
38
39 return result = x++;
40 }
41 //]
42
43 template<typename T>
44 class pushable {
45 #ifndef BOOST_CONTRACT_NO_ALL
46 friend class boost::contract::access;
47 #endif
48
49 #ifndef BOOST_CONTRACT_NO_INVARIANTS
invariant() const50 void invariant() const {
51 BOOST_CONTRACT_ASSERT(capacity() <= max_size());
52 }
53 #endif
54
55 public:
56 virtual void push_back(
57 T const& x
58 #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
59 , boost::contract::virtual_* v = 0
60 #endif
61 ) = 0;
62
63 protected:
64 virtual unsigned capacity() const = 0;
65 virtual unsigned max_size() const = 0;
66 };
67
68 template<typename T>
push_back(T const & x,boost::contract::virtual_ * v)69 void pushable<T>::push_back(
70 T const& x
71 #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
72 , boost::contract::virtual_* v
73 #endif
74 ) {
75 #ifndef BOOST_CONTRACT_NO_OLDS
76 boost::contract::old_ptr<unsigned> old_capacity =
77 BOOST_CONTRACT_OLDOF(v, capacity());
78 #endif
79 #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
80 boost::contract::check c = boost::contract::public_function(v, this)
81 #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
82 .precondition([&] {
83 BOOST_CONTRACT_ASSERT(capacity() < max_size());
84 })
85 #endif
86 #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
87 .postcondition([&] {
88 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
89 })
90 #endif
91 ;
92 #endif
93 assert(false); // Shall never execute this body.
94 }
95
96 //[ifdef_class
97 class integers
98 #define BASES public pushable<int>
99 :
100 #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
101 private boost::contract::constructor_precondition<integers>, BASES
102 #else
103 BASES
104 #endif
105 {
106 #ifndef BOOST_CONTRACT_NO_ALL
107 friend class boost::contract::access;
108 #endif
109
110 #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
111 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
112 #endif
113 #undef BASES
114
115 #ifndef BOOST_CONTRACT_NO_INVARIANTS
invariant() const116 void invariant() const {
117 BOOST_CONTRACT_ASSERT(size() <= capacity());
118 }
119 #endif
120
121 public:
integers(int from,int to)122 integers(int from, int to) :
123 #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
124 boost::contract::constructor_precondition<integers>([&] {
125 BOOST_CONTRACT_ASSERT(from <= to);
126 }),
127 #endif
128 vect_(to - from + 1)
129 {
130 #ifndef BOOST_CONTRACT_NO_CONSTRUCTORS
131 boost::contract::check c = boost::contract::constructor(this)
132 #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
__anonecd9e8980602null133 .postcondition([&] {
134 BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1));
135 })
136 #endif
137 ;
138 #endif
139
140 for(int x = from; x <= to; ++x) vect_.at(x - from) = x;
141 }
142
~integers()143 virtual ~integers() {
144 #ifndef BOOST_CONTRACT_NO_DESTRUCTORS
145 // Check invariants.
146 boost::contract::check c = boost::contract::destructor(this);
147 #endif
148 }
149
push_back(int const & x,boost::contract::virtual_ * v=0)150 virtual void push_back(
151 int const& x
152 #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
153 , boost::contract::virtual_* v = 0
154 #endif
155 ) /* override */ {
156 #ifndef BOOST_CONTRACT_NO_OLDS
157 boost::contract::old_ptr<unsigned> old_size;
158 #endif
159 #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
160 boost::contract::check c = boost::contract::public_function<
161 override_push_back>(v, &integers::push_back, this, x)
162 #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
163 .precondition([&] {
164 BOOST_CONTRACT_ASSERT(size() < max_size());
165 })
166 #endif
167 #ifndef BOOST_CONTRACT_NO_OLDS
168 .old([&] {
169 old_size = BOOST_CONTRACT_OLDOF(v, size());
170 })
171 #endif
172 #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
173 .postcondition([&] {
174 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
175 })
176 #endif
177 #ifndef BOOST_CONTRACT_NO_EXCEPTS
178 .except([&] {
179 BOOST_CONTRACT_ASSERT(size() == *old_size);
180 })
181 #endif
182 ;
183 #endif
184
185 vect_.push_back(x);
186 }
187
188 private:
189 #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
190 BOOST_CONTRACT_OVERRIDE(push_back)
191 #endif
192
193 /* ... */
194 //]
195
196 public: // Could program contracts for these too...
size() const197 unsigned size() const { return vect_.size(); }
max_size() const198 unsigned max_size() const { return vect_.max_size(); }
capacity() const199 unsigned capacity() const { return vect_.capacity(); }
200
201 private:
202 std::vector<int> vect_;
203 };
204
main()205 int main() {
206 integers i(1, 10);
207 int x = 123;
208 i.push_back(inc(x));
209 assert(x == 124);
210 assert(i.size() == 11);
211 return 0;
212 }
213
214