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 <iostream>
11 #include <cassert>
12
13 //[assertion_level_no_impl
14 // If valid iterator range (cannot implement in C++ but OK to use in AXIOM).
15 template<typename Iter>
16 bool valid(Iter first, Iter last); // Only declared, not actually defined.
17 //]
18
19 //[assertion_level_class_begin
20 template<typename T>
21 class vector {
22 //]
23
24 public:
25 typedef typename std::vector<T>::iterator iterator;
26
27 // Could program class invariants and contracts for the following.
begin()28 iterator begin() { return vect_.begin(); }
end()29 iterator end() { return vect_.end(); }
capacity() const30 unsigned capacity() const { return vect_.capacity(); }
operator ==(vector const & other)31 bool operator==(vector const& other) { return vect_ == other.vect_; }
32
33 //[assertion_level_axiom
34 public:
insert(iterator where,T const & value)35 iterator insert(iterator where, T const& value) {
36 iterator result;
37 boost::contract::old_ptr<unsigned> old_capacity =
38 BOOST_CONTRACT_OLDOF(capacity());
39 boost::contract::check c = boost::contract::public_function(this)
40 .postcondition([&] {
41 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
42 if(capacity() > *old_capacity) {
43 BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end()));
44 } else {
45 BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end()));
46 }
47 })
48 ;
49
50 return result = vect_.insert(where, value);
51 }
52 //]
53
54 //[assertion_level_audit_old
55 public:
swap(vector & other)56 void swap(vector& other) {
57 boost::contract::old_ptr<vector> old_me, old_other;
58 #ifdef BOOST_CONTRACT_AUDITS
59 old_me = BOOST_CONTRACT_OLDOF(*this);
60 old_other = BOOST_CONTRACT_OLDOF(other);
61 #endif // Else, skip old value copies...
62 boost::contract::check c = boost::contract::public_function(this)
63 .postcondition([&] {
64 // ...and also skip related assertions.
65 BOOST_CONTRACT_ASSERT_AUDIT(*this == *old_other);
66 BOOST_CONTRACT_ASSERT_AUDIT(other == *old_me);
67 })
68 ;
69
70 vect_.swap(other.vect_);
71 }
72 //]
73
74 //[assertion_level_class_end
75 /* ... */
76
77 private:
78 std::vector<T> vect_;
79 };
80 //]
81
82 //[assertion_level_audit
83 template<typename RandomIter, typename T>
random_binary_search(RandomIter first,RandomIter last,T const & value)84 RandomIter random_binary_search(RandomIter first, RandomIter last,
85 T const& value) {
86 RandomIter result;
87 boost::contract::check c = boost::contract::function()
88 .precondition([&] {
89 BOOST_CONTRACT_ASSERT(first <= last); // Default, not expensive.
90 // Expensive O(n) assertion (use AXIOM if prohibitive instead).
91 BOOST_CONTRACT_ASSERT_AUDIT(std::is_sorted(first, last));
92 })
93 .postcondition([&] {
94 if(result != last) BOOST_CONTRACT_ASSERT(*result == value);
95 })
96 ;
97
98 /* ... */
99 //]
100
101 RandomIter begin = first, end = last;
102 while(begin < end) {
103 RandomIter middle = begin + ((end - begin) >> 1);
104 BOOST_CONTRACT_CHECK(*begin <= *middle || value < *middle ||
105 *middle < value);
106
107 if(value < *middle) end = middle;
108 else if(value > *middle) begin = middle + 1;
109 else return result = middle;
110 }
111 return result = last;
112 }
113
main()114 int main() {
115 vector<char> v;
116 v.insert(v.begin() + 0, 'a');
117 v.insert(v.begin() + 1, 'b');
118 v.insert(v.begin() + 2, 'c');
119
120 vector<char>::iterator i = random_binary_search(v.begin(), v.end(), 'b');
121 assert(i != v.end());
122 assert(*i == 'b');
123
124 vector<char> w;
125 w.insert(w.begin() + 0, 'x');
126 w.insert(w.begin() + 1, 'y');
127
128 w.swap(v);
129 assert(*(w.begin() + 0) == 'a');
130 assert(*(w.begin() + 1) == 'b');
131 assert(*(w.begin() + 2) == 'c');
132
133 return 0;
134 }
135
136