139 lines
3.6 KiB
C++
139 lines
3.6 KiB
C++
|
|
// 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
|
|
|
|
//[mitchell02_stack
|
|
#include <boost/contract.hpp>
|
|
#include <boost/optional.hpp>
|
|
#include <vector>
|
|
#include <cassert>
|
|
|
|
template<typename T>
|
|
class stack {
|
|
friend class boost::contract::access;
|
|
|
|
void invariant() const {
|
|
BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
|
|
}
|
|
|
|
public:
|
|
/* Creation */
|
|
|
|
// Create empty stack.
|
|
stack() {
|
|
boost::contract::check c = boost::contract::constructor(this)
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(count() == 0); // Empty.
|
|
})
|
|
;
|
|
}
|
|
|
|
// Destroy stack.
|
|
virtual ~stack() {
|
|
// Check invariants.
|
|
boost::contract::check c = boost::contract::destructor(this);
|
|
}
|
|
|
|
/* Basic Queries */
|
|
|
|
// Number of items.
|
|
int count() const {
|
|
// Check invariants.
|
|
boost::contract::check c = boost::contract::public_function(this);
|
|
return items_.size();
|
|
}
|
|
|
|
// Item at index in [1, count()] (as in Eiffel).
|
|
T const& item_at(int index) const {
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.precondition([&] {
|
|
BOOST_CONTRACT_ASSERT(index > 0); // Positive index.
|
|
BOOST_CONTRACT_ASSERT(index <= count()); // Index within count.
|
|
})
|
|
;
|
|
|
|
return items_[index - 1];
|
|
}
|
|
|
|
/* Derived Queries */
|
|
|
|
// If no items.
|
|
bool is_empty() const {
|
|
bool result;
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.postcondition([&] {
|
|
// Consistent with count.
|
|
BOOST_CONTRACT_ASSERT(result == (count() == 0));
|
|
})
|
|
;
|
|
|
|
return result = (count() == 0);
|
|
}
|
|
|
|
// Top item.
|
|
T const& item() const {
|
|
boost::optional<T const&> result; // Avoid extra construction of T.
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.precondition([&] {
|
|
BOOST_CONTRACT_ASSERT(count() > 0); // Not empty.
|
|
})
|
|
.postcondition([&] {
|
|
// Item on top.
|
|
BOOST_CONTRACT_ASSERT(*result == item_at(count()));
|
|
})
|
|
;
|
|
|
|
return *(result = item_at(count()));
|
|
}
|
|
|
|
/* Commands */
|
|
|
|
// Push item to the top.
|
|
void put(T const& new_item) {
|
|
boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc.
|
|
BOOST_CONTRACT_ASSERT(item() == new_item); // Item set.
|
|
})
|
|
;
|
|
|
|
items_.push_back(new_item);
|
|
}
|
|
|
|
// Pop top item.
|
|
void remove() {
|
|
boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.precondition([&] {
|
|
BOOST_CONTRACT_ASSERT(count() > 0); // Not empty.
|
|
})
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec.
|
|
})
|
|
;
|
|
|
|
items_.pop_back();
|
|
}
|
|
|
|
private:
|
|
std::vector<T> items_;
|
|
};
|
|
|
|
int main() {
|
|
stack<int> s;
|
|
assert(s.count() == 0);
|
|
|
|
s.put(123);
|
|
assert(s.item() == 123);
|
|
|
|
s.remove();
|
|
assert(s.is_empty());
|
|
|
|
return 0;
|
|
}
|
|
//]
|
|
|