136 lines
4.0 KiB
C++
136 lines
4.0 KiB
C++
|
|
// 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 <vector>
|
|
#include <algorithm>
|
|
#include <iostream>
|
|
#include <cassert>
|
|
|
|
//[assertion_level_no_impl
|
|
// If valid iterator range (cannot implement in C++ but OK to use in AXIOM).
|
|
template<typename Iter>
|
|
bool valid(Iter first, Iter last); // Only declared, not actually defined.
|
|
//]
|
|
|
|
//[assertion_level_class_begin
|
|
template<typename T>
|
|
class vector {
|
|
//]
|
|
|
|
public:
|
|
typedef typename std::vector<T>::iterator iterator;
|
|
|
|
// Could program class invariants and contracts for the following.
|
|
iterator begin() { return vect_.begin(); }
|
|
iterator end() { return vect_.end(); }
|
|
unsigned capacity() const { return vect_.capacity(); }
|
|
bool operator==(vector const& other) { return vect_ == other.vect_; }
|
|
|
|
//[assertion_level_axiom
|
|
public:
|
|
iterator insert(iterator where, T const& value) {
|
|
iterator result;
|
|
boost::contract::old_ptr<unsigned> old_capacity =
|
|
BOOST_CONTRACT_OLDOF(capacity());
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
|
|
if(capacity() > *old_capacity) {
|
|
BOOST_CONTRACT_ASSERT_AXIOM(!valid(begin(), end()));
|
|
} else {
|
|
BOOST_CONTRACT_ASSERT_AXIOM(!valid(where, end()));
|
|
}
|
|
})
|
|
;
|
|
|
|
return result = vect_.insert(where, value);
|
|
}
|
|
//]
|
|
|
|
//[assertion_level_audit_old
|
|
public:
|
|
void swap(vector& other) {
|
|
boost::contract::old_ptr<vector> old_me, old_other;
|
|
#ifdef BOOST_CONTRACT_AUDITS
|
|
old_me = BOOST_CONTRACT_OLDOF(*this);
|
|
old_other = BOOST_CONTRACT_OLDOF(other);
|
|
#endif // Else, skip old value copies...
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.postcondition([&] {
|
|
// ...and also skip related assertions.
|
|
BOOST_CONTRACT_ASSERT_AUDIT(*this == *old_other);
|
|
BOOST_CONTRACT_ASSERT_AUDIT(other == *old_me);
|
|
})
|
|
;
|
|
|
|
vect_.swap(other.vect_);
|
|
}
|
|
//]
|
|
|
|
//[assertion_level_class_end
|
|
/* ... */
|
|
|
|
private:
|
|
std::vector<T> vect_;
|
|
};
|
|
//]
|
|
|
|
//[assertion_level_audit
|
|
template<typename RandomIter, typename T>
|
|
RandomIter random_binary_search(RandomIter first, RandomIter last,
|
|
T const& value) {
|
|
RandomIter result;
|
|
boost::contract::check c = boost::contract::function()
|
|
.precondition([&] {
|
|
BOOST_CONTRACT_ASSERT(first <= last); // Default, not expensive.
|
|
// Expensive O(n) assertion (use AXIOM if prohibitive instead).
|
|
BOOST_CONTRACT_ASSERT_AUDIT(std::is_sorted(first, last));
|
|
})
|
|
.postcondition([&] {
|
|
if(result != last) BOOST_CONTRACT_ASSERT(*result == value);
|
|
})
|
|
;
|
|
|
|
/* ... */
|
|
//]
|
|
|
|
RandomIter begin = first, end = last;
|
|
while(begin < end) {
|
|
RandomIter middle = begin + ((end - begin) >> 1);
|
|
BOOST_CONTRACT_CHECK(*begin <= *middle || value < *middle ||
|
|
*middle < value);
|
|
|
|
if(value < *middle) end = middle;
|
|
else if(value > *middle) begin = middle + 1;
|
|
else return result = middle;
|
|
}
|
|
return result = last;
|
|
}
|
|
|
|
int main() {
|
|
vector<char> v;
|
|
v.insert(v.begin() + 0, 'a');
|
|
v.insert(v.begin() + 1, 'b');
|
|
v.insert(v.begin() + 2, 'c');
|
|
|
|
vector<char>::iterator i = random_binary_search(v.begin(), v.end(), 'b');
|
|
assert(i != v.end());
|
|
assert(*i == 'b');
|
|
|
|
vector<char> w;
|
|
w.insert(w.begin() + 0, 'x');
|
|
w.insert(w.begin() + 1, 'y');
|
|
|
|
w.swap(v);
|
|
assert(*(w.begin() + 0) == 'a');
|
|
assert(*(w.begin() + 1) == 'b');
|
|
assert(*(w.begin() + 2) == 'c');
|
|
|
|
return 0;
|
|
}
|
|
|