123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145 |
- // 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;
- }
- //]
|