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 <boost/optional.hpp>
9 #include <vector>
10 #include <cassert>
11
12 template<typename T>
13 class accessible {
14 public:
15 virtual T& at(unsigned index, boost::contract::virtual_* v = 0) = 0;
16
17 // Could program class invariants and contracts for following too.
18 virtual T const& operator[](unsigned index) const = 0;
19 virtual unsigned size() const = 0;
20 };
21
22 //[optional_result_virtual
23 template<typename T>
at(unsigned index,boost::contract::virtual_ * v)24 T& accessible<T>::at(unsigned index, boost::contract::virtual_* v) {
25 boost::optional<T&> result;
26 // Pass `result` right after `v`...
27 boost::contract::check c = boost::contract::public_function(v, result, this)
28 .precondition([&] {
29 BOOST_CONTRACT_ASSERT(index < size());
30 })
31 // ...plus postconditions take `result` as a parameter (not capture).
32 .postcondition([&] (boost::optional<T const&> const& result) {
33 BOOST_CONTRACT_ASSERT(*result == operator[](index));
34 })
35 ;
36
37 assert(false);
38 return *result;
39 }
40 //]
41
42 template<typename T>
43 class vector
44 #define BASES public accessible<T>
45 : BASES
46 {
47 public:
48 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
49 #undef BASES
50
at(unsigned index,boost::contract::virtual_ * v=0)51 T& at(unsigned index, boost::contract::virtual_* v = 0) /* override */ {
52 boost::optional<T&> result;
53 // Pass `result` right after `v`...
54 boost::contract::check c = boost::contract::public_function<
55 override_at>(v, result, &vector::at, this, index)
56 // ...plus postconditions take `result` as parameter (not capture).
57 .postcondition([&] (boost::optional<T const&> const& result) {
58 if(index == 0) BOOST_CONTRACT_ASSERT(*result == front());
59 })
60 ;
61
62 return *(result = vect_[index]);
63 }
64
65 // Could program class invariants and contracts for following too.
operator [](unsigned index) const66 T const& operator[](unsigned index) const { return vect_[index]; }
size() const67 unsigned size() const { return vect_.size(); }
front() const68 T const& front() const { return vect_.front(); }
push_back(T const & value)69 void push_back(T const& value) { vect_.push_back(value); }
70
71 BOOST_CONTRACT_OVERRIDE(at)
72
73 private:
74 std::vector<T> vect_;
75 };
76
main()77 int main() {
78 vector<int> v;
79 v.push_back(123);
80 v.push_back(456);
81 v.push_back(789);
82 int& x = v.at(1);
83 assert(x == 456);
84 x = -456;
85 assert(v.at(1) == -456);
86 return 0;
87 }
88
89