123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135 |
- // 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;
- }
|