240 lines
7.2 KiB
C++
240 lines
7.2 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
|
|
|
|
//[cline90_vstack
|
|
#include "vector.hpp"
|
|
#include <boost/contract.hpp>
|
|
#include <boost/optional.hpp>
|
|
#include <cassert>
|
|
|
|
// NOTE: Incomplete contract assertions, addressing only `empty` and `full`.
|
|
template<typename T>
|
|
class abstract_stack {
|
|
public:
|
|
abstract_stack() {
|
|
boost::contract::check c = boost::contract::constructor(this)
|
|
.postcondition([&] {
|
|
// AXIOM as empty() cannot actually be checked here to avoid
|
|
// calling pure virtual function length() during construction).
|
|
BOOST_CONTRACT_ASSERT_AXIOM(empty());
|
|
})
|
|
;
|
|
}
|
|
|
|
virtual ~abstract_stack() {
|
|
boost::contract::check c = boost::contract::destructor(this);
|
|
}
|
|
|
|
bool full() const {
|
|
bool result;
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(result == (length() == capacity()));
|
|
})
|
|
;
|
|
|
|
return result = (length() == capacity());
|
|
}
|
|
|
|
bool empty() const {
|
|
bool result;
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(result = (length() == 0));
|
|
})
|
|
;
|
|
|
|
return result = (length() == 0);
|
|
}
|
|
|
|
virtual int length(boost::contract::virtual_* v = 0) const = 0;
|
|
virtual int capacity(boost::contract::virtual_* v = 0) const = 0;
|
|
|
|
virtual T const& item(boost::contract::virtual_* v = 0) const = 0;
|
|
|
|
virtual void push(T const& value, boost::contract::virtual_* v = 0) = 0;
|
|
virtual T const& pop(boost::contract::virtual_* v = 0) = 0;
|
|
|
|
virtual void clear(boost::contract::virtual_* v = 0) = 0;
|
|
};
|
|
|
|
template<typename T>
|
|
int abstract_stack<T>::length(boost::contract::virtual_* v) const {
|
|
int result;
|
|
boost::contract::check c = boost::contract::public_function(v, result, this)
|
|
.postcondition([&] (int const& result) {
|
|
BOOST_CONTRACT_ASSERT(result >= 0);
|
|
})
|
|
;
|
|
assert(false);
|
|
return result;
|
|
}
|
|
|
|
template<typename T>
|
|
int abstract_stack<T>::capacity(boost::contract::virtual_* v) const {
|
|
int result;
|
|
boost::contract::check c = boost::contract::public_function(v, result, this)
|
|
.postcondition([&] (int const& result) {
|
|
BOOST_CONTRACT_ASSERT(result >= 0);
|
|
})
|
|
;
|
|
assert(false);
|
|
return result;
|
|
}
|
|
|
|
template<typename T>
|
|
T const& abstract_stack<T>::item(boost::contract::virtual_* v) const {
|
|
boost::optional<T const&> result;
|
|
boost::contract::check c = boost::contract::public_function(v, result, this)
|
|
.precondition([&] {
|
|
BOOST_CONTRACT_ASSERT(!empty());
|
|
})
|
|
;
|
|
assert(false);
|
|
return *result;
|
|
}
|
|
|
|
template<typename T>
|
|
void abstract_stack<T>::push(T const& value, boost::contract::virtual_* v) {
|
|
boost::contract::check c = boost::contract::public_function(v, this)
|
|
.precondition([&] {
|
|
BOOST_CONTRACT_ASSERT(!full());
|
|
})
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(!empty());
|
|
})
|
|
;
|
|
assert(false);
|
|
}
|
|
|
|
template<typename T>
|
|
T const& abstract_stack<T>::pop(boost::contract::virtual_* v) {
|
|
boost::optional<T const&> result;
|
|
boost::contract::old_ptr<T> old_item = BOOST_CONTRACT_OLDOF(v, item());
|
|
boost::contract::check c = boost::contract::public_function(v, result, this)
|
|
.precondition([&] {
|
|
BOOST_CONTRACT_ASSERT(!empty());
|
|
})
|
|
.postcondition([&] (boost::optional<T const&> const& result) {
|
|
BOOST_CONTRACT_ASSERT(!full());
|
|
BOOST_CONTRACT_ASSERT(*result == *old_item);
|
|
})
|
|
;
|
|
assert(false);
|
|
return *result;
|
|
}
|
|
|
|
template<typename T>
|
|
void abstract_stack<T>::clear(boost::contract::virtual_* v) {
|
|
boost::contract::check c = boost::contract::public_function(v, this)
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(empty());
|
|
})
|
|
;
|
|
assert(false);
|
|
}
|
|
|
|
template<typename T>
|
|
class vstack
|
|
#define BASES private boost::contract::constructor_precondition< \
|
|
vstack<T> >, public abstract_stack<T>
|
|
: BASES
|
|
{
|
|
friend class boost::contract::access;
|
|
|
|
typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
|
|
#undef BASES
|
|
|
|
void invariant() const {
|
|
BOOST_CONTRACT_ASSERT(length() >= 0);
|
|
BOOST_CONTRACT_ASSERT(length() < capacity());
|
|
}
|
|
|
|
BOOST_CONTRACT_OVERRIDES(length, capacity, item, push, pop, clear)
|
|
|
|
public:
|
|
explicit vstack(int count = 10) :
|
|
boost::contract::constructor_precondition<vstack>([&] {
|
|
BOOST_CONTRACT_ASSERT(count >= 0);
|
|
}),
|
|
vect_(count), // OK, executed after precondition so count >= 0.
|
|
len_(0)
|
|
{
|
|
boost::contract::check c = boost::contract::constructor(this)
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(length() == 0);
|
|
BOOST_CONTRACT_ASSERT(capacity() == count);
|
|
})
|
|
;
|
|
}
|
|
|
|
virtual ~vstack() {
|
|
boost::contract::check c = boost::contract::destructor(this);
|
|
}
|
|
|
|
// Inherited from abstract_stack.
|
|
|
|
virtual int length(boost::contract::virtual_* v = 0) const /* override */ {
|
|
int result;
|
|
boost::contract::check c = boost::contract::public_function<
|
|
override_length>(v, result, &vstack::length, this);
|
|
return result = len_;
|
|
}
|
|
|
|
virtual int capacity(boost::contract::virtual_* v = 0)
|
|
const /* override */ {
|
|
int result;
|
|
boost::contract::check c = boost::contract::public_function<
|
|
override_capacity>(v, result, &vstack::capacity, this);
|
|
return result = vect_.size();
|
|
}
|
|
|
|
virtual T const& item(boost::contract::virtual_* v = 0)
|
|
const /* override */ {
|
|
boost::optional<T const&> result;
|
|
boost::contract::check c = boost::contract::public_function<
|
|
override_item>(v, result, &vstack::item, this);
|
|
return *(result = vect_[len_ - 1]);
|
|
}
|
|
|
|
virtual void push(T const& value, boost::contract::virtual_* v = 0)
|
|
/* override */ {
|
|
boost::contract::check c = boost::contract::public_function<
|
|
override_push>(v, &vstack::push, this, value);
|
|
vect_[len_++] = value;
|
|
}
|
|
|
|
virtual T const& pop(boost::contract::virtual_* v = 0) /* override */ {
|
|
boost::optional<T const&> result;
|
|
boost::contract::check c = boost::contract::public_function<
|
|
override_pop>(v, result, &vstack::pop, this);
|
|
return *(result = vect_[--len_]);
|
|
}
|
|
|
|
virtual void clear(boost::contract::virtual_* v = 0) /* override */ {
|
|
boost::contract::check c = boost::contract::public_function<
|
|
override_clear>(v, &vstack::clear, this);
|
|
len_ = 0;
|
|
}
|
|
|
|
private:
|
|
vector<T> vect_;
|
|
int len_;
|
|
};
|
|
|
|
int main() {
|
|
vstack<int> s(3);
|
|
assert(s.capacity() == 3);
|
|
|
|
s.push(123);
|
|
assert(s.length() == 1);
|
|
assert(s.pop() == 123);
|
|
|
|
return 0;
|
|
}
|
|
//]
|
|
|