finished example section. recompiled all tests and examples.

This commit is contained in:
Lorenzo Caminiti
2016-05-12 08:22:34 -07:00
parent 0c8a75df83
commit 1aa41fd14e
48 changed files with 1812 additions and 1593 deletions

View File

@@ -3,26 +3,26 @@
#include "vector.hpp"
#include <boost/contract.hpp>
#include <boost/optional.hpp>
#include <boost/detail/lightweight_test.hpp>
#include <cassert>
// NOTE: Incomplete contract assertions, addressing `empty` and `full` only.
template<typename T>
class abstract_stack {
public:
// NOTE: Incomplete contract assertions, addressing `empty` and `full` only.
abstract_stack() {
auto c = boost::contract::constructor(this)
boost::contract::guard c = boost::contract::constructor(this)
// Postcondition: empty() (but it cannot be checked here to avoid
// calling pure virtual function length() during construction).
;
}
virtual ~abstract_stack() { auto c = boost::contract::destructor(this); }
virtual ~abstract_stack() {
boost::contract::guard c = boost::contract::destructor(this);
}
bool full() const {
bool result;
auto c = boost::contract::public_function(this)
boost::contract::guard c = boost::contract::public_function(this)
.postcondition([&] {
BOOST_CONTRACT_ASSERT(result == (length() == capacity()));
})
@@ -33,7 +33,7 @@ public:
bool empty() const {
bool result;
auto c = boost::contract::public_function(this)
boost::contract::guard c = boost::contract::public_function(this)
.postcondition([&] {
BOOST_CONTRACT_ASSERT(result = (length() == 0));
})
@@ -56,38 +56,42 @@ public:
template<typename T>
int abstract_stack<T>::length(boost::contract::virtual_* v) const {
int result;
auto c = boost::contract::public_function(v, result, this)
boost::contract::guard c = boost::contract::public_function(v, result, this)
.postcondition([&] (int const& result) {
BOOST_CONTRACT_ASSERT(result >= 0);
})
;
assert(false); return result;
assert(false);
return result;
}
template<typename T>
int abstract_stack<T>::capacity(boost::contract::virtual_* v) const {
int result;
auto c = boost::contract::public_function(v, result, this)
boost::contract::guard c = boost::contract::public_function(v, result, this)
.postcondition([&] (int const& result) {
BOOST_CONTRACT_ASSERT(result >= 0);
})
;
assert(false); return result;
assert(false);
return result;
}
template<typename T>
T const& abstract_stack<T>::item(boost::contract::virtual_* v) const {
auto c = boost::contract::public_function(v, this)
boost::optional<T const&> result;
boost::contract::guard c = boost::contract::public_function(v, result, this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(!empty());
})
;
assert(false); return *boost::optional<T const&>();
assert(false);
return *result;
}
template<typename T>
void abstract_stack<T>::push(T const& value, boost::contract::virtual_* v) {
auto c = boost::contract::public_function(v, this)
boost::contract::guard c = boost::contract::public_function(v, this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(!full());
})
@@ -101,8 +105,8 @@ void abstract_stack<T>::push(T const& value, boost::contract::virtual_* v) {
template<typename T>
T const& abstract_stack<T>::pop(boost::contract::virtual_* v) {
boost::optional<T const&> result;
auto old_item = BOOST_CONTRACT_OLDOF(v, item());
auto c = boost::contract::public_function(v, result, this)
boost::contract::old_ptr<T> old_item = BOOST_CONTRACT_OLDOF(v, item());
boost::contract::guard c = boost::contract::public_function(v, result, this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(!empty());
})
@@ -111,14 +115,15 @@ T const& abstract_stack<T>::pop(boost::contract::virtual_* v) {
BOOST_CONTRACT_ASSERT(*result == *old_item);
})
;
assert(false); return *boost::optional<T const&>();
assert(false);
return *result;
}
template<typename T>
void abstract_stack<T>::clear(boost::contract::virtual_* v) {
auto c = boost::contract::public_function(v, this)
boost::contract::guard c = boost::contract::public_function(v, this)
.postcondition([&] {
BOOST_CONTRACT_ASSERT(this->empty());
BOOST_CONTRACT_ASSERT(empty());
})
;
assert(false);
@@ -130,15 +135,17 @@ class vstack
vstack<T> >, public abstract_stack<T>
: BASES
{
public:
friend class boost::contract::access;
typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
#undef BASES
BOOST_CONTRACT_OVERRIDES(length, capacity, item, push, pop, clear)
void invariant() const {
BOOST_CONTRACT_ASSERT(length() >= 0);
BOOST_CONTRACT_ASSERT(length() < capacity());
}
public:
explicit vstack(int count = 10) :
boost::contract::constructor_precondition<vstack>([&] {
BOOST_CONTRACT_ASSERT(count >= 0);
@@ -146,7 +153,7 @@ public:
vect_(count), // OK, executed after precondition so count >= 0.
len_(0)
{
auto c = boost::contract::constructor(this)
boost::contract::guard c = boost::contract::constructor(this)
.postcondition([&] {
BOOST_CONTRACT_ASSERT(length() == 0);
BOOST_CONTRACT_ASSERT(capacity() == count);
@@ -154,58 +161,54 @@ public:
;
}
virtual ~vstack() { auto c = boost::contract::destructor(this); }
virtual ~vstack() {
boost::contract::guard c = boost::contract::destructor(this);
}
// Inherited from abstract_stack.
virtual int length(boost::contract::virtual_* v = 0) const /* override */ {
int result;
auto c = boost::contract::public_function<override_length>(
v, result, &vstack::length, this);
boost::contract::guard c = boost::contract::public_function<
override_length>(v, result, &vstack::length, this);
return result = len_;
}
BOOST_CONTRACT_OVERRIDE(length)
virtual int capacity(boost::contract::virtual_* v = 0)
const /* override */ {
int result;
auto c = boost::contract::public_function<override_capacity>(
v, result, &vstack::capacity, this);
boost::contract::guard c = boost::contract::public_function<
override_capacity>(v, result, &vstack::capacity, this);
return result = vect_.size();
}
BOOST_CONTRACT_OVERRIDE(capacity)
virtual T const& item(boost::contract::virtual_* v = 0)
const /* override */ {
boost::optional<T const&> result;
auto c = boost::contract::public_function<override_item>(
v, result, &vstack::item, this);
boost::contract::guard c = boost::contract::public_function<
override_item>(v, result, &vstack::item, this);
return *(result = vect_[len_ - 1]);
}
BOOST_CONTRACT_OVERRIDE(item)
virtual void push(T const& value, boost::contract::virtual_* v = 0)
/* override */ {
auto c = boost::contract::public_function<override_push>(
v, &vstack::push, this, value);
boost::contract::guard c = boost::contract::public_function<
override_push>(v, &vstack::push, this, value);
vect_[len_++] = value;
}
BOOST_CONTRACT_OVERRIDE(push)
virtual T const& pop(boost::contract::virtual_* v = 0) /* override */ {
boost::optional<T const&> result;
auto c = boost::contract::public_function<override_pop>(
v, result, &vstack::pop, this);
boost::contract::guard c = boost::contract::public_function<
override_pop>(v, result, &vstack::pop, this);
return *(result = vect_[--len_]);
}
BOOST_CONTRACT_OVERRIDE(pop)
virtual void clear(boost::contract::virtual_* v = 0) /* override */ {
auto c = boost::contract::public_function<override_clear>(
v, &vstack::clear, this);
boost::contract::guard c = boost::contract::public_function<
override_clear>(v, &vstack::clear, this);
len_ = 0;
}
BOOST_CONTRACT_OVERRIDE(clear);
private:
vector<T> vect_;
@@ -214,13 +217,13 @@ private:
int main() {
vstack<int> s(3);
BOOST_TEST_EQ(s.capacity(), 3);
assert(s.capacity() == 3);
s.push(123);
BOOST_TEST_EQ(s.length(), 1);
BOOST_TEST_EQ(s.pop(), 123);
assert(s.length() == 1);
assert(s.pop() == 123);
return boost::report_errors();
return 0;
}
//]