146 lines
4.2 KiB
C++
146 lines
4.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
|
|
|
|
//[mitchell02_name_list
|
|
#include <boost/contract.hpp>
|
|
#include <string>
|
|
#include <vector>
|
|
#include <algorithm>
|
|
#include <cassert>
|
|
|
|
// List of names.
|
|
class name_list {
|
|
friend class boost::contract::access;
|
|
|
|
void invariant() const {
|
|
BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
|
|
}
|
|
|
|
public:
|
|
/* Creation */
|
|
|
|
// Create an empty list.
|
|
name_list() {
|
|
boost::contract::check c = boost::contract::constructor(this)
|
|
.postcondition([&] {
|
|
BOOST_CONTRACT_ASSERT(count() == 0); // Empty list.
|
|
})
|
|
;
|
|
}
|
|
|
|
// Destroy list.
|
|
virtual ~name_list() {
|
|
// Check invariants.
|
|
boost::contract::check c = boost::contract::destructor(this);
|
|
}
|
|
|
|
/* Basic Queries */
|
|
|
|
// Number of names in list.
|
|
int count() const {
|
|
// Check invariants.
|
|
boost::contract::check c = boost::contract::public_function(this);
|
|
return names_.size();
|
|
}
|
|
|
|
// Is name in list?
|
|
bool has(std::string const& name) const {
|
|
bool result;
|
|
boost::contract::check c = boost::contract::public_function(this)
|
|
.postcondition([&] {
|
|
// If empty, has not.
|
|
if(count() == 0) BOOST_CONTRACT_ASSERT(!result);
|
|
})
|
|
;
|
|
|
|
return result = names_.cend() != std::find(names_.cbegin(),
|
|
names_.cend(), name);
|
|
}
|
|
|
|
/* Commands */
|
|
|
|
// Add name to list, if name not already in list.
|
|
virtual void put(std::string const& name,
|
|
boost::contract::virtual_* v = 0) {
|
|
boost::contract::old_ptr<bool> old_has_name =
|
|
BOOST_CONTRACT_OLDOF(v, has(name));
|
|
boost::contract::old_ptr<int> old_count =
|
|
BOOST_CONTRACT_OLDOF(v, count());
|
|
boost::contract::check c = boost::contract::public_function(v, this)
|
|
.precondition([&] {
|
|
BOOST_CONTRACT_ASSERT(!has(name)); // Not already in list.
|
|
})
|
|
.postcondition([&] {
|
|
if(!*old_has_name) { // If-guard allows to relax subcontracts.
|
|
BOOST_CONTRACT_ASSERT(has(name)); // Name in list.
|
|
BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Inc.
|
|
}
|
|
})
|
|
;
|
|
|
|
names_.push_back(name);
|
|
}
|
|
|
|
private:
|
|
std::vector<std::string> names_;
|
|
};
|
|
|
|
class relaxed_name_list
|
|
#define BASES public name_list
|
|
: BASES
|
|
{
|
|
friend class boost::contract::access;
|
|
|
|
typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting.
|
|
#undef BASES
|
|
|
|
BOOST_CONTRACT_OVERRIDE(put);
|
|
|
|
public:
|
|
/* Commands */
|
|
|
|
// Add name to list, or do nothing if name already in list (relaxed).
|
|
void put(std::string const& name,
|
|
boost::contract::virtual_* v = 0) /* override */ {
|
|
boost::contract::old_ptr<bool> old_has_name =
|
|
BOOST_CONTRACT_OLDOF(v, has(name));
|
|
boost::contract::old_ptr<int> old_count =
|
|
BOOST_CONTRACT_OLDOF(v, count());
|
|
boost::contract::check c = boost::contract::public_function<
|
|
override_put>(v, &relaxed_name_list::put, this, name)
|
|
.precondition([&] { // Relax inherited preconditions.
|
|
BOOST_CONTRACT_ASSERT(has(name)); // Already in list.
|
|
})
|
|
.postcondition([&] { // Inherited post. not checked given if-guard.
|
|
if(*old_has_name) {
|
|
// Count unchanged if name already in list.
|
|
BOOST_CONTRACT_ASSERT(count() == *old_count);
|
|
}
|
|
})
|
|
;
|
|
|
|
if(!has(name)) name_list::put(name); // Else, do nothing.
|
|
}
|
|
};
|
|
|
|
int main() {
|
|
std::string const js = "John Smith";
|
|
|
|
relaxed_name_list rl;
|
|
rl.put(js);
|
|
assert(rl.has(js));
|
|
rl.put(js); // OK, relaxed contracts allow calling this again (do nothing).
|
|
|
|
name_list nl;
|
|
nl.put(js);
|
|
assert(nl.has(js));
|
|
// nl.put(js); // Error, contracts do not allow calling this again.
|
|
|
|
return 0;
|
|
}
|
|
//]
|
|
|