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
18int 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(f: [&] {
27 BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max());
28 })
29 #endif
30 #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
31 .postcondition(f: [&] {
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
43template<typename T>
44class pushable {
45 #ifndef BOOST_CONTRACT_NO_ALL
46 friend class boost::contract::access;
47 #endif
48
49 #ifndef BOOST_CONTRACT_NO_INVARIANTS
50 void invariant() const {
51 BOOST_CONTRACT_ASSERT(capacity() <= max_size());
52 }
53 #endif
54
55public:
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
63protected:
64 virtual unsigned capacity() const = 0;
65 virtual unsigned max_size() const = 0;
66};
67
68template<typename T>
69void 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
97class 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
116 void invariant() const {
117 BOOST_CONTRACT_ASSERT(size() <= capacity());
118 }
119 #endif
120
121public:
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(obj: this)
132 #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
133 .postcondition(f: [&] {
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(n: x - from) = x;
141 }
142
143 virtual ~integers() {
144 #ifndef BOOST_CONTRACT_NO_DESTRUCTORS
145 // Check invariants.
146 boost::contract::check c = boost::contract::destructor(obj: this);
147 #endif
148 }
149
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, obj: this, args: x)
162 #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
163 .precondition(f: [&] {
164 BOOST_CONTRACT_ASSERT(size() < max_size());
165 })
166 #endif
167 #ifndef BOOST_CONTRACT_NO_OLDS
168 .old(f: [&] {
169 old_size = BOOST_CONTRACT_OLDOF(v, size());
170 })
171 #endif
172 #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
173 .postcondition(f: [&] {
174 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
175 })
176 #endif
177 #ifndef BOOST_CONTRACT_NO_EXCEPTS
178 .except(f: [&] {
179 BOOST_CONTRACT_ASSERT(size() == *old_size);
180 })
181 #endif
182 ;
183 #endif
184
185 vect_.push_back(x: x);
186 }
187
188private:
189 #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
190 BOOST_CONTRACT_OVERRIDE(push_back)
191 #endif
192
193 /* ... */
194//]
195
196public: // Could program contracts for these too...
197 unsigned size() const { return vect_.size(); }
198 unsigned max_size() const { return vect_.max_size(); }
199 unsigned capacity() const { return vect_.capacity(); }
200
201private:
202 std::vector<int> vect_;
203};
204
205int main() {
206 integers i(1, 10);
207 int x = 123;
208 i.push_back(x: inc(x));
209 assert(x == 124);
210 assert(i.size() == 11);
211 return 0;
212}
213
214

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