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 <cassert> 10 11 //[pure_virtual_public_base_begin 12 template<typename Iterator> 13 class range { 14 public: 15 // Pure virtual function declaration (contract in definition below). 16 virtual Iterator begin(boost::contract::virtual_* v = 0) = 0; 17 //] 18 19 // Could program class invariants and contracts for the following too. 20 virtual Iterator end() = 0; 21 virtual bool empty() const = 0; 22 23 //[pure_virtual_public_base_end 24 /* ... */ 25 }; 26 //] 27 28 //[pure_virtual_public_base_impl 29 // Pure virtual function default implementation (out-of-line in C++). 30 template<typename Iterator> begin(boost::contract::virtual_ * v)31Iterator range<Iterator>::begin(boost::contract::virtual_* v) { 32 Iterator result; // As usual, virtual pass `result` right after `v`... 33 boost::contract::check c = boost::contract::public_function(v, result, this) 34 .postcondition([&] (Iterator const& result) { 35 if(empty()) BOOST_CONTRACT_ASSERT(result == end()); 36 }) 37 ; 38 39 // Pure function body (never executed by this library). 40 assert(false); 41 return result; 42 } 43 //] 44 45 template<typename T> 46 class vector 47 #define BASES public range<typename std::vector<T>::iterator> 48 : BASES 49 { 50 public: 51 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; 52 #undef BASES 53 typedef typename std::vector<T>::iterator iterator; 54 begin(boost::contract::virtual_ * v=0)55 iterator begin(boost::contract::virtual_* v = 0) /* override */ { 56 iterator result; 57 // Again, pass result right after `v`... 58 boost::contract::check c = boost::contract::public_function< 59 override_begin>(v, result, &vector::begin, this) 60 // ...plus postconditions take `result` as parameter (not capture). 61 .postcondition([&] (iterator const& result) { 62 if(!empty()) BOOST_CONTRACT_ASSERT(*result == front()); 63 }) 64 ; 65 66 return result = vect_.begin(); 67 } BOOST_CONTRACT_OVERRIDE(begin)68 BOOST_CONTRACT_OVERRIDE(begin) 69 70 // Could program class invariants and contracts for the following too. 71 iterator end() { return vect_.end(); } empty() const72 bool empty() const { return vect_.empty(); } front() const73 T const& front() const { return vect_.front(); } push_back(T const & value)74 void push_back(T const& value) { vect_.push_back(value); } 75 76 private: 77 std::vector<T> vect_; 78 }; 79 main()80int main() { 81 vector<int> v; 82 v.push_back(1); 83 v.push_back(2); 84 v.push_back(3); 85 range<std::vector<int>::iterator>& r = v; 86 assert(*(r.begin()) == 1); 87 return 0; 88 } 89 90