123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725 |
- // 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
- //[n1962_vector_n1962
- // Extra spaces, newlines, etc. for visual alignment with this library code.
- #include <boost/algorithm/cxx11/all_of.hpp>
- #include <boost/type_traits/has_equal_to.hpp>
- #include <boost/next_prior.hpp>
- #include <vector>
- #include <iterator>
- #include <memory>
- template< class T, class Allocator = std::allocator<T> >
- class vector {
-
-
- invariant {
- empty() == (size() == 0);
- std::distance(begin(), end()) == int(size());
- std::distance(rbegin(), rend()) == int(size());
- size() <= capacity();
- capacity() <= max_size();
- }
- public:
- typedef typename std::vector<T, Allocator>::allocator_type allocator_type;
- typedef typename std::vector<T, Allocator>::pointer pointer;
- typedef typename std::vector<T, Allocator>::const_pointer const_pointer;
- typedef typename std::vector<T, Allocator>::reference reference;
- typedef typename std::vector<T, Allocator>::const_reference const_reference;
- typedef typename std::vector<T, Allocator>::value_type value_type;
- typedef typename std::vector<T, Allocator>::iterator iterator;
- typedef typename std::vector<T, Allocator>::const_iterator const_iterator;
- typedef typename std::vector<T, Allocator>::size_type size_type;
- typedef typename std::vector<T, Allocator>::difference_type difference_type;
- typedef typename std::vector<T, Allocator>::reverse_iterator
- reverse_iterator;
- typedef typename std::vector<T, Allocator>::const_reverse_iterator
- const_reverse_iterator;
- vector()
- postcondition {
- empty();
- }
- : vect_()
- {}
-
-
- explicit vector(Allocator const& alloc)
- postcondition {
- empty();
- get_allocator() == alloc;
- }
- : vect_(alloc)
- {}
-
- explicit vector(size_type count)
- postcondition {
- size() == count;
- if constexpr(boost::has_equal_to<T>::value) {
- boost::algorithm::all_of_equal(begin(), end(), T());
- }
- }
- : vect_(count)
- {}
-
-
-
- vector(size_type count, T const& value)
- postcondition {
- size() == count;
- if constexpr(boost::has_equal_to<T>::value) {
- boost::algorithm::all_of_equal(begin(), end(), value);
- }
- }
- : vect_(count, value)
- {}
-
-
-
-
- vector(size_type count, T const& value, Allocator const& alloc)
- postcondition {
- size() == count;
- if constexpr(boost::has_equal_to<T>::value) {
- boost::algorithm::all_of_equal(begin(), end(), value);
- }
- get_allocator() == alloc;
- }
- : vect_(count, value, alloc)
- {}
-
-
-
-
- template<typename InputIter>
- vector(InputIter first, InputIter last)
- postcondition {
- std::distance(first, last) == int(size());
- }
- : vect_(first, last)
- {}
-
- template<typename InputIter>
- vector(InputIter first, InputIter last, Allocator const& alloc)
- postcondition {
- std::distance(first, last) == int(size());
- get_allocator() == alloc;
- }
- : vect_(first, last, alloc)
- {}
-
-
- /* implicit */ vector(vector const& other)
- postcondition {
- if constexpr(boost::has_equal_to<T>::value) {
- *this == other;
- }
- }
- : vect_(other.vect_)
- {}
-
-
-
- vector& operator=(vector const& other)
- postcondition(result) {
- if constexpr(boost::has_equal_to<T>::value) {
- *this == other;
- result == *this;
- }
- }
- {
- if(this != &other) vect_ = other.vect_;
- return *this;
- }
-
-
-
-
-
-
-
-
- virtual ~vector() {}
-
-
- void reserve(size_type count)
- precondition {
- count < max_size();
- }
- postcondition {
- capacity() >= count;
- }
- {
- vect_.reserve(count);
- }
-
- size_type capacity() const
- postcondition(result) {
- result >= size();
- }
- {
- return vect_.capacity();
- }
-
-
- iterator begin()
- postcondition {
- if(empty()) result == end();
- }
- {
- return vect_.begin();
- }
-
-
- const_iterator begin() const
- postcondition(result) {
- if(empty()) result == end();
- }
- {
- return vect_.begin();
- }
-
-
- iterator end() {
- return vect_.end();
- }
- const_iterator end() const {
- return vect_.end();
- }
-
- reverse_iterator rbegin()
- postcondition(result) {
- if(empty()) result == rend();
- }
- {
- return vect_.rbegin();
- }
-
-
- const_reverse_iterator rbegin() const
- postcondition(result) {
- if(empty()) result == rend();
- }
- {
- return vect_.rbegin();
- }
-
-
- reverse_iterator rend() {
- return vect_.rend();
- }
-
- const_reverse_iterator rend() const {
- return vect_.rend();
- }
- void resize(size_type count, T const& value = T())
- postcondition {
- size() == count;
- if constexpr(boost::has_equal_to<T>::value) {
- if(count > oldof(size())) {
- boost::algorithm::all_of_equal(begin() + oldof(size()),
- end(), value);
- }
- }
- }
- {
- vect_.resize(count, value);
- }
-
-
-
-
- size_type size() const
- postcondition(result) {
- result <= capacity();
- }
- {
- return vect_.size();
- }
-
-
- size_type max_size() const
- postcondition(result) {
- result >= capacity();
- }
- {
- return vect_.max_size();
- }
-
-
- bool empty() const
- postcondition(result) {
- result == (size() == 0);
- }
- {
- return vect_.empty();
- }
-
-
- Alloctor get_allocator() const {
- return vect_.get_allocator();
- }
-
- reference at(size_type index) {
- // No precondition (throw out_of_range for invalid index).
- return vect_.at(index);
- }
- const_reference at(size_type index) const {
- // No precondition (throw out_of_range for invalid index).
- return vect_.at(index);
- }
- reference operator[](size_type index)
- precondition {
- index < size();
- }
- {
- return vect_[index];
- }
-
- const_reference operator[](size_type index) const
- precondition {
- index < size();
- }
- {
- return vect_[index];
- }
-
- reference front()
- precondition {
- !empty();
- }
- {
- return vect_.front();
- }
-
- const_reference front() const
- precondition {
- !empty();
- }
- {
- return vect_.front();
- }
-
- reference back()
- precondition {
- !empty();
- }
- {
- return vect_.back();
- }
-
- const_reference back() const
- precondition {
- !empty();
- }
- {
- return vect_.back();
- }
-
- void push_back(T const& value)
- precondition {
- size() < max_size();
- }
- postcondition {
- size() == oldof(size()) + 1;
- capacity() >= oldof(capacity())
- if constexpr(boost::has_equal_to<T>::value) {
- back() == value;
- }
- }
- {
- vect_.push_back(value);
- }
-
-
-
-
-
-
-
-
- void pop_back()
- precondition {
- !empty();
- }
- postcondition {
- size() == oldof(size()) - 1;
- }
- {
- vect_.pop_back();
- }
-
-
-
- template<typename InputIter>
- void assign(InputIter first, InputIter last)
- // Precondition: [begin(), end()) does not contain [first, last).
- postcondition {
- std::distance(first, last) == int(size());
- }
- {
- vect_.assign(first, last);
- }
-
-
-
-
-
- void assign(size_type count, T const& vallue)
- precondition {
- count <= max_size();
- }
- postcondition {
- if constexpr(boost::has_equal_to<T>::value) {
- boost::algorithm::all_of_equal(begin(), end(), value);
- }
- }
- {
- vect_.assign(count, value);
- }
-
-
-
-
- iterator insert(iterator where, T const& value)
- precondition {
- size() < max_size();
- }
- postcondition(result) {
- size() == oldof(size()) + 1;
- capacity() >= oldof(capacity());
- if constexpr(boost::has_equal_to<T>::value) {
- *result == value;
- }
- // if(capacity() > oldof(capacity()))
- // [begin(), end()) is invalid
- // else
- // [where, end()) is invalid
- }
- {
- return vect_.insert(where, value);
- }
-
-
-
-
-
-
-
-
-
-
- void insert(iterator where, size_type count, T const& value)
- precondition {
- size() + count < max_size();
- }
- postcondition {
- size() == oldof(size()) + count;
- capacity() >= oldof(capacity());
- if(capacity() == oldof(capacity())) {
- if constexpr(boost::has_equal_to<T>::value) {
- boost::algorithm::all_of_equal(boost::prior(oldof(where)),
- boost::prior(oldof(where)) + count, value);
- }
- // [where, end()) is invalid
- }
- // else [begin(), end()) is invalid
- }
- {
- vect_.insert(where, count, value);
- }
-
-
-
-
-
-
-
-
-
-
-
- template<typename InputIter>
- void insert(iterator where, Iterator first, Iterator last)
- precondition {
- size() + std::distance(first, last) < max_size();
- // [first, last) is not contained in [begin(), end())
- }
- postcondition {
- size() == oldof(size()) + std::distance(first, last);
- capacity() >= oldof(capacity());
- if(capacity() == oldof(capacity())) {
- if constexpr(boost::has_equal_to<T>::value) {
- boost::algorithm::all_of_equal(first, last, oldof(where));
- }
- // [where, end()) is invalid
- }
- // else [begin(), end()) is invalid
- }
- {
- vect_.insert(where, first, last);
- }
-
-
-
-
-
-
-
-
-
-
-
-
- iterator erase(iterator where)
- precondition {
- !empty();
- where != end();
- }
- postcondition(result) {
- size() == oldod size() - 1;
- if(empty()) result == end();
- // [where, end()) is invalid
- }
- {
- return vect_.erase(where);
- }
-
-
-
-
- iterator erase(iterator first, iterator last)
- precondition {
- size() >= std::distance(first, lasst);
- }
- postcondition(result) {
- size() == oldof(size()) - std::distance(first, last);
- if(empty()) result == end();
- // [first, last) is invalid
- }
- {
- return vect_.erase(first, last);
- }
-
-
-
-
-
-
- void clear()
- postcondition {
- empty();
- }
- {
- vect_.clear();
- }
- void swap(vector& other)
- precondition {
- get_allocator() == other.get_allocator();
- }
- postcondition {
- if constexpr(boost::has_equal_to<T>::value) {
- *this == oldof(other);
- other == oldof(*this);
- }
- }
- {
- vect_.swap(other);
- }
-
-
- friend bool operator==(vector const& left, vector const& right) {
- // Cannot check class invariants for left and right objects.
- return left.vect_ == right.vect_;
- }
- private:
- std::vector<T, Allocator> vect_;
- };
- // End.
- //]
|