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 //[cline90_vector 8 #ifndef VECTOR_HPP_ 9 #define VECTOR_HPP_ 10 11 #include <boost/contract.hpp> 12 13 // NOTE: Incomplete contract assertions, addressing only `size`. 14 template<typename T> 15 class vector 16 #define BASES private boost::contract::constructor_precondition<vector<T> > 17 : BASES 18 { 19 friend class boost::contract::access; 20 21 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; 22 #undef BASES 23 invariant() const24 void invariant() const { 25 BOOST_CONTRACT_ASSERT(size() >= 0); 26 } 27 28 public: vector(int count=10)29 explicit vector(int count = 10) : 30 boost::contract::constructor_precondition<vector>([&] { 31 BOOST_CONTRACT_ASSERT(count >= 0); 32 }), 33 data_(new T[count]), 34 size_(count) 35 { 36 boost::contract::check c = boost::contract::constructor(this) __anon3561b5c70202null37 .postcondition([&] { 38 BOOST_CONTRACT_ASSERT(size() == count); 39 }) 40 ; 41 42 for(int i = 0; i < size_; ++i) data_[i] = T(); 43 } 44 ~vector()45 virtual ~vector() { 46 boost::contract::check c = boost::contract::destructor(this); 47 delete[] data_; 48 } 49 size() const50 int size() const { 51 boost::contract::check c = boost::contract::public_function(this); 52 return size_; // Non-negative result already checked by invariant. 53 } 54 resize(int count)55 void resize(int count) { 56 boost::contract::check c = boost::contract::public_function(this) 57 .precondition([&] { 58 BOOST_CONTRACT_ASSERT(count >= 0); 59 }) 60 .postcondition([&] { 61 BOOST_CONTRACT_ASSERT(size() == count); 62 }) 63 ; 64 65 T* slice = new T[count]; 66 for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i]; 67 delete[] data_; 68 data_ = slice; 69 size_ = count; 70 } 71 operator [](int index)72 T& operator[](int index) { 73 boost::contract::check c = boost::contract::public_function(this) 74 .precondition([&] { 75 BOOST_CONTRACT_ASSERT(index >= 0); 76 BOOST_CONTRACT_ASSERT(index < size()); 77 }) 78 ; 79 80 return data_[index]; 81 } 82 operator [](int index) const83 T const& operator[](int index) const { 84 boost::contract::check c = boost::contract::public_function(this) 85 .precondition([&] { 86 BOOST_CONTRACT_ASSERT(index >= 0); 87 BOOST_CONTRACT_ASSERT(index < size()); 88 }) 89 ; 90 91 return data_[index]; 92 } 93 94 private: 95 T* data_; 96 int size_; 97 }; 98 99 #endif // #include guard 100 //] 101 102