1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
// Copyright (C) 2008-2018 Lorenzo Caminiti
// Distributed under the Boost Software License, Version 1.0 (see accompanying
// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
#include <boost/contract.hpp>
#include <boost/optional.hpp>
#include <vector>
#include <cassert>
template<typename T>
class accessible {
public:
virtual T& at(unsigned index, boost::contract::virtual_* v = 0) = 0;
// Could program class invariants and contracts for following too.
virtual T const& operator[](unsigned index) const = 0;
virtual unsigned size() const = 0;
};
//[optional_result_virtual
template<typename T>
T& accessible<T>::at(unsigned index, boost::contract::virtual_* v) {
boost::optional<T&> result;
// Pass `result` right after `v`...
boost::contract::check c = boost::contract::public_function(v, result, this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(index < size());
})
// ...plus postconditions take `result` as a parameter (not capture).
.postcondition([&] (boost::optional<T const&> const& result) {
BOOST_CONTRACT_ASSERT(*result == operator[](index));
})
;
assert(false);
return *result;
}
//]
template<typename T>
class vector
#define BASES public accessible<T>
: BASES
{
public:
typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
#undef BASES
T& at(unsigned index, boost::contract::virtual_* v = 0) /* override */ {
boost::optional<T&> result;
// Pass `result` right after `v`...
boost::contract::check c = boost::contract::public_function<
override_at>(v, result, &vector::at, this, index)
// ...plus postconditions take `result` as parameter (not capture).
.postcondition([&] (boost::optional<T const&> const& result) {
if(index == 0) BOOST_CONTRACT_ASSERT(*result == front());
})
;
return *(result = vect_[index]);
}
// Could program class invariants and contracts for following too.
T const& operator[](unsigned index) const { return vect_[index]; }
unsigned size() const { return vect_.size(); }
T const& front() const { return vect_.front(); }
void push_back(T const& value) { vect_.push_back(value); }
BOOST_CONTRACT_OVERRIDE(at)
private:
std::vector<T> vect_;
};
int main() {
vector<int> v;
v.push_back(123);
v.push_back(456);
v.push_back(789);
int& x = v.at(1);
assert(x == 456);
x = -456;
assert(v.at(1) == -456);
return 0;
}
|
