123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101 |
- // 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
- //[cline90_vector
- #ifndef VECTOR_HPP_
- #define VECTOR_HPP_
- #include <boost/contract.hpp>
- // NOTE: Incomplete contract assertions, addressing only `size`.
- template<typename T>
- class vector
- #define BASES private boost::contract::constructor_precondition<vector<T> >
- : BASES
- {
- friend class boost::contract::access;
- typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
- #undef BASES
- void invariant() const {
- BOOST_CONTRACT_ASSERT(size() >= 0);
- }
- public:
- explicit vector(int count = 10) :
- boost::contract::constructor_precondition<vector>([&] {
- BOOST_CONTRACT_ASSERT(count >= 0);
- }),
- data_(new T[count]),
- size_(count)
- {
- boost::contract::check c = boost::contract::constructor(this)
- .postcondition([&] {
- BOOST_CONTRACT_ASSERT(size() == count);
- })
- ;
- for(int i = 0; i < size_; ++i) data_[i] = T();
- }
- virtual ~vector() {
- boost::contract::check c = boost::contract::destructor(this);
- delete[] data_;
- }
- int size() const {
- boost::contract::check c = boost::contract::public_function(this);
- return size_; // Non-negative result already checked by invariant.
- }
- void resize(int count) {
- boost::contract::check c = boost::contract::public_function(this)
- .precondition([&] {
- BOOST_CONTRACT_ASSERT(count >= 0);
- })
- .postcondition([&] {
- BOOST_CONTRACT_ASSERT(size() == count);
- })
- ;
- T* slice = new T[count];
- for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i];
- delete[] data_;
- data_ = slice;
- size_ = count;
- }
- T& operator[](int index) {
- boost::contract::check c = boost::contract::public_function(this)
- .precondition([&] {
- BOOST_CONTRACT_ASSERT(index >= 0);
- BOOST_CONTRACT_ASSERT(index < size());
- })
- ;
- return data_[index];
- }
-
- T const& operator[](int index) const {
- boost::contract::check c = boost::contract::public_function(this)
- .precondition([&] {
- BOOST_CONTRACT_ASSERT(index >= 0);
- BOOST_CONTRACT_ASSERT(index < size());
- })
- ;
- return data_[index];
- }
- private:
- T* data_;
- int size_;
- };
- #endif // #include guard
- //]
|