libs/contract/example/features/base_types_no_macro.cpp
// 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
#include <boost/contract.hpp>
#include <vector>
#include <algorithm>
#include <cassert>
template<typename T>
class pushable {
public:
void invariant() const {
BOOST_CONTRACT_ASSERT(capacity() <= max_size());
}
virtual void push_back(T x, boost::contract::virtual_* v = 0) = 0;
protected:
virtual unsigned capacity() const = 0;
virtual unsigned max_size() const = 0;
};
template<typename T>
void pushable<T>::push_back(T x, boost::contract::virtual_* v) {
boost::contract::old_ptr<unsigned> old_capacity =
BOOST_CONTRACT_OLDOF(v, capacity());
boost::contract::check c = boost::contract::public_function(v, this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(capacity() < max_size());
})
.postcondition([&] {
BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
})
;
assert(false); // Shall never execute this body.
}
struct has_size { virtual unsigned size() const = 0; };
struct has_empty { virtual bool empty() const = 0; };
class unique_chars
: private boost::contract::constructor_precondition<unique_chars>
{
public:
void invariant() const {
BOOST_CONTRACT_ASSERT(size() >= 0);
}
unique_chars(char from, char to) :
boost::contract::constructor_precondition<unique_chars>([&] {
BOOST_CONTRACT_ASSERT(from <= to);
})
{
boost::contract::check c = boost::contract::constructor(this)
.postcondition([&] {
BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1));
})
;
for(char x = from; x <= to; ++x) vect_.push_back(x);
}
virtual ~unique_chars() {
boost::contract::check c = boost::contract::destructor(this);
}
unsigned size() const {
boost::contract::check c = boost::contract::public_function(this);
return vect_.size();
}
bool find(char x) const {
bool result;
boost::contract::check c = boost::contract::public_function(this)
.postcondition([&] {
if(size() == 0) BOOST_CONTRACT_ASSERT(!result);
})
;
return result = std::find(vect_.begin(), vect_.end(), x) != vect_.end();
}
virtual void push_back(char x, boost::contract::virtual_* v = 0) {
boost::contract::old_ptr<bool> old_find =
BOOST_CONTRACT_OLDOF(v, find(x));
boost::contract::old_ptr<unsigned> old_size =
BOOST_CONTRACT_OLDOF(v, size());
boost::contract::check c = boost::contract::public_function(v, this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(!find(x));
})
.postcondition([&] {
if(!*old_find) {
BOOST_CONTRACT_ASSERT(find(x));
BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
}
})
;
vect_.push_back(x);
}
protected:
unique_chars() {}
std::vector<char> const& vect() const { return vect_; }
private:
std::vector<char> vect_;
};
//[base_types_no_macro
#include <boost/mpl/vector.hpp>
class chars :
private boost::contract::constructor_precondition<chars>,
public unique_chars,
public virtual pushable<char>,
virtual protected has_size,
private has_empty
{
public:
// Program `base_types` without macros (list only public bases).
typedef boost::mpl::vector<unique_chars, pushable<char> > base_types;
/* ... */
//]
void invariant() const {
BOOST_CONTRACT_ASSERT(empty() == (size() == 0));
}
chars(char from, char to) : unique_chars(from, to) {
boost::contract::check c = boost::contract::constructor(this);
}
chars(char const* const c_str) :
boost::contract::constructor_precondition<chars>([&] {
BOOST_CONTRACT_ASSERT(c_str[0] != '\0');
})
{
boost::contract::check c = boost::contract::constructor(this);
for(unsigned i = 0; c_str[i] != '\0'; ++i) push_back(c_str[i]);
}
void push_back(char x, boost::contract::virtual_* v = 0) /* override */ {
boost::contract::old_ptr<bool> old_find =
BOOST_CONTRACT_OLDOF(v, find(x));
boost::contract::old_ptr<unsigned> old_size =
BOOST_CONTRACT_OLDOF(v, size());
boost::contract::check c = boost::contract::public_function<
override_push_back>(v, &chars::push_back, this, x)
.precondition([&] {
BOOST_CONTRACT_ASSERT(find(x));
})
.postcondition([&] {
if(*old_find) BOOST_CONTRACT_ASSERT(size() == *old_size);
})
;
if(!find(x)) unique_chars::push_back(x);
}
BOOST_CONTRACT_OVERRIDE(push_back);
bool empty() const {
boost::contract::check c = boost::contract::public_function(this);
return size() == 0;
}
unsigned size() const { return unique_chars::size(); }
protected:
unsigned max_size() const { return vect().max_size(); }
unsigned capacity() const { return vect().capacity(); }
};
int main() {
chars s("abc");
assert(s.find('a'));
assert(s.find('b'));
assert(!s.find('x'));
return 0;
}