• Home
  • Line#
  • Scopes#
  • Navigate#
  • Raw
  • Download
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 //[public_class_begin
13 class unique_identifiers :
14     private boost::contract::constructor_precondition<unique_identifiers>
15 {
16 public:
invariant() const17     void invariant() const {
18         BOOST_CONTRACT_ASSERT(size() >= 0);
19     }
20 //]
21 
22 //[public_constructor
23 public:
24     // Contract for a constructor.
unique_identifiers(int from,int to)25     unique_identifiers(int from, int to) :
26         boost::contract::constructor_precondition<unique_identifiers>([&] {
27             BOOST_CONTRACT_ASSERT(from >= 0);
28             BOOST_CONTRACT_ASSERT(to >= from);
29         })
30     {
31         boost::contract::check c = boost::contract::constructor(this)
__anon5a7596b70202null32             .postcondition([&] {
33                 BOOST_CONTRACT_ASSERT(size() == (to - from + 1));
34             })
35         ;
36 
37         // Constructor body.
38         for(int id = from; id <= to; ++id) vect_.push_back(id);
39     }
40 //]
41 
42 //[public_destructor
43 public:
44     // Contract for a destructor.
~unique_identifiers()45     virtual ~unique_identifiers() {
46         // Following contract checks class invariants.
47         boost::contract::check c = boost::contract::destructor(this);
48 
49         // Destructor body here... (do nothing in this example).
50     }
51 //]
52 
size() const53     int size() const {
54         // Following contract checks invariants.
55         boost::contract::check c = boost::contract::public_function(this);
56         return vect_.size();
57     }
58 
59 //[public_function
60 public:
61     // Contract for a public function (but no static, virtual, or override).
find(int id) const62     bool find(int id) const {
63         bool result;
64         boost::contract::check c = boost::contract::public_function(this)
65             .precondition([&] {
66                 BOOST_CONTRACT_ASSERT(id >= 0);
67             })
68             .postcondition([&] {
69                 if(size() == 0) BOOST_CONTRACT_ASSERT(!result);
70             })
71         ;
72 
73         // Function body.
74         return result = std::find(vect_.begin(), vect_.end(), id) !=
75                 vect_.end();
76     }
77 //]
78 
79 //[public_virtual_function
80 public:
81     // Contract for a public virtual function (but no override).
push_back(int id,boost::contract::virtual_ * v=0)82     virtual int push_back(int id, boost::contract::virtual_* v = 0) { // Extra `v`.
83         int result;
84         boost::contract::old_ptr<bool> old_find =
85                 BOOST_CONTRACT_OLDOF(v, find(id)); // Pass `v`.
86         boost::contract::old_ptr<int> old_size =
87                 BOOST_CONTRACT_OLDOF(v, size()); // Pass `v`.
88         boost::contract::check c = boost::contract::public_function(
89                 v, result, this) // Pass `v` and `result`.
90             .precondition([&] {
91                 BOOST_CONTRACT_ASSERT(id >= 0);
92                 BOOST_CONTRACT_ASSERT(!find(id)); // ID cannot be already present.
93             })
94             .postcondition([&] (int const result) {
95                 if(!*old_find) {
96                     BOOST_CONTRACT_ASSERT(find(id));
97                     BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
98                 }
99                 BOOST_CONTRACT_ASSERT(result == id);
100             })
101         ;
102 
103         // Function body.
104         vect_.push_back(id);
105         return result = id;
106     }
107 //]
108 
109 private:
110     std::vector<int> vect_;
111 //[public_class_end
112     /* ... */
113 };
114 //]
115 
116 //[public_derived_class_begin
117 class identifiers
118     #define BASES public unique_identifiers
119     : BASES
120 {
121 public:
122     typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Bases typedef.
123     #undef BASES
124 
invariant() const125     void invariant() const { // Check in AND with bases.
126         BOOST_CONTRACT_ASSERT(empty() == (size() == 0));
127     }
128 //]
129 
130 //[public_function_override
131 public:
132     // Contract for a public function override.
push_back(int id,boost::contract::virtual_ * v=0)133     int push_back(int id, boost::contract::virtual_* v = 0) /* override */ {
134         int result;
135         boost::contract::old_ptr<bool> old_find =
136                 BOOST_CONTRACT_OLDOF(v, find(id));
137         boost::contract::old_ptr<int> old_size =
138                 BOOST_CONTRACT_OLDOF(v, size());
139         boost::contract::check c = boost::contract::public_function<
140             override_push_back // Pass override type plus below function pointer...
141         >(v, result, &identifiers::push_back, this, id) // ...and arguments.
142             .precondition([&] { // Check in OR with bases.
143                 BOOST_CONTRACT_ASSERT(id >= 0);
144                 BOOST_CONTRACT_ASSERT(find(id)); // ID can be already present.
145             })
146             .postcondition([&] (int const result) { // Check in AND with bases.
147                 if(*old_find) BOOST_CONTRACT_ASSERT(size() == *old_size);
148             })
149         ;
150 
151         // Function body.
152         if(!find(id)) unique_identifiers::push_back(id); // Else, do nothing.
153         return result = id;
154     }
BOOST_CONTRACT_OVERRIDE(push_back)155     BOOST_CONTRACT_OVERRIDE(push_back) // Define `override_push_back`.
156 //]
157 
158     bool empty() const {
159         // Following contract checks invariants.
160         boost::contract::check c = boost::contract::public_function(this);
161         return size() == 0;
162     }
163 
identifiers(int from,int to)164     identifiers(int from, int to) : unique_identifiers(from, to) {
165         // Following contract checks invariants.
166         boost::contract::check c = boost::contract::constructor(this);
167     }
168 
169 //[public_derived_class_end
170     /* ... */
171 };
172 //]
173 
main()174 int main() {
175     unique_identifiers uids(1, 4);
176     assert(uids.find(2));
177     assert(!uids.find(5));
178     uids.push_back(5);
179     assert(uids.find(5));
180 
181     identifiers ids(10, 40);
182     assert(!ids.find(50));
183     ids.push_back(50);
184     ids.push_back(50);
185     assert(ids.find(50));
186 
187     return 0;
188 }
189 
190