diff options
Diffstat (limited to 'src/boost/libs/contract/example/mitchell02')
13 files changed, 1648 insertions, 0 deletions
diff --git a/src/boost/libs/contract/example/mitchell02/counter/counter.hpp b/src/boost/libs/contract/example/mitchell02/counter/counter.hpp new file mode 100644 index 00000000..659edbe9 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/counter/counter.hpp @@ -0,0 +1,71 @@ + +// 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_counter +#ifndef COUNTER_HPP_ +#define COUNTER_HPP_ + +#include "../observer/subject.hpp" +#include <boost/contract.hpp> + +class counter + #define BASES public subject + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + +public: + /* Creation */ + + // Construct counter with specified value. + explicit counter(int a_value = 10) : value_(a_value) { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(value() == a_value); // Value set. + }) + ; + } + + // Destroy counter. + virtual ~counter() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Queries */ + + // Current counter value. + int value() const { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::public_function(this); + return value_; + } + + /* Commands */ + + // Decrement counter value. + void decrement() { + boost::contract::old_ptr<int> old_value = BOOST_CONTRACT_OLDOF(value()); + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(value() == *old_value - 1); // Decrement. + }) + ; + + --value_; + notify(); // Notify all attached observers. + } + +private: + int value_; +}; + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/counter/decrement_button.hpp b/src/boost/libs/contract/example/mitchell02/counter/decrement_button.hpp new file mode 100644 index 00000000..ba8ae67e --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/counter/decrement_button.hpp @@ -0,0 +1,94 @@ + +// 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_decrement_button +#ifndef DECREMENT_BUTTON_HPP_ +#define DECREMENT_BUTTON_HPP_ + +#include "push_button.hpp" +#include "counter.hpp" +#include "../observer/observer.hpp" +#include <boost/contract.hpp> +#include <boost/noncopyable.hpp> + +class decrement_button + #define BASES public push_button, public observer, \ + private boost::noncopyable + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + BOOST_CONTRACT_OVERRIDES(on_bn_clicked, up_to_date_with_subject, update); + +public: + /* Creation */ + + explicit decrement_button(counter& a_counter) : counter_(a_counter) { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + // Enable iff positive value. + BOOST_CONTRACT_ASSERT(enabled() == (a_counter.value() > 0)); + }) + ; + counter_.attach(this); + } + + // Destroy button. + virtual ~decrement_button() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Commands */ + + virtual void on_bn_clicked(boost::contract::virtual_* v = 0) + /* override */ { + boost::contract::old_ptr<int> old_value = + BOOST_CONTRACT_OLDOF(v, counter_.value()); + boost::contract::check c = boost::contract::public_function< + override_on_bn_clicked + >(v, &decrement_button::on_bn_clicked, this) + .postcondition([&] { + // Counter decremented. + BOOST_CONTRACT_ASSERT(counter_.value() == *old_value - 1); + }) + ; + counter_.decrement(); + } + + virtual bool up_to_date_with_subject(boost::contract::virtual_* v = 0) + const /* override */ { + bool result; + boost::contract::check c = boost::contract::public_function< + override_up_to_date_with_subject + >(v, result, &decrement_button::up_to_date_with_subject, this); + + return result = true; // For simplicity, assume always up-to-date. + } + + virtual void update(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_update>(v, &decrement_button::update, this) + .postcondition([&] { + // Enabled iff positive value. + BOOST_CONTRACT_ASSERT(enabled() == (counter_.value() > 0)); + }) + ; + + if(counter_.value() == 0) disable(); + else enable(); + } + +private: + counter& counter_; +}; + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/counter/push_button.hpp b/src/boost/libs/contract/example/mitchell02/counter/push_button.hpp new file mode 100644 index 00000000..eaa66f79 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/counter/push_button.hpp @@ -0,0 +1,86 @@ + +// 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_push_button +#ifndef PUSH_BUTTON_HPP_ +#define PUSH_BUTTON_HPP_ + +#include <boost/contract.hpp> +#include <cassert> + +class push_button { +public: + // No inv and no bases so contracts optional if no pre, post, and override. + + /* Creation */ + + // Create an enabled button. + push_button() : enabled_(true) { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(enabled()); // Enabled. + }) + ; + } + + // Destroy button. + virtual ~push_button() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Queries */ + + // If button is enabled. + bool enabled() const { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::public_function(this); + return enabled_; + } + + /* Commands */ + + // Enable button. + void enable() { + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(enabled()); // Enabled. + }) + ; + + enabled_ = true; + } + + // Disable button. + void disable() { + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(!enabled()); // Disabled. + }) + ; + + enabled_ = false; + } + + // Invoke externally when button clicked. + virtual void on_bn_clicked(boost::contract::virtual_* v = 0) = 0; + +private: + bool enabled_; +}; + +void push_button::on_bn_clicked(boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(enabled()); // Enabled. + }) + ; + assert(false); +} + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/counter_main.cpp b/src/boost/libs/contract/example/mitchell02/counter_main.cpp new file mode 100644 index 00000000..ace7b8b9 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/counter_main.cpp @@ -0,0 +1,81 @@ + +// 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_counter_main +#include "counter/counter.hpp" +#include "counter/decrement_button.hpp" +#include "observer/observer.hpp" +#include <cassert> + +int test_counter; + +class view_of_counter + #define BASES public observer + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + BOOST_CONTRACT_OVERRIDES(up_to_date_with_subject, update) + +public: + /* Creation */ + + // Create view associated with given counter. + explicit view_of_counter(counter& a_counter) : counter_(a_counter) { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::constructor(this); + + counter_.attach(this); + assert(counter_.value() == test_counter); + } + + // Destroy view. + virtual ~view_of_counter() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Commands */ + + virtual bool up_to_date_with_subject(boost::contract::virtual_* v = 0) + const /* override */ { + bool result; + boost::contract::check c = boost::contract::public_function< + override_up_to_date_with_subject + >(v, result, &view_of_counter::up_to_date_with_subject, this); + + return result = true; // For simplicity, assume always up-to-date. + } + + virtual void update(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_update>(v, &view_of_counter::update, this); + + assert(counter_.value() == test_counter); + } + +private: + counter& counter_; +}; + +int main() { + counter cnt(test_counter = 1); + view_of_counter view(cnt); + + decrement_button dec(cnt); + assert(dec.enabled()); + + test_counter--; + dec.on_bn_clicked(); + assert(!dec.enabled()); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/courier.cpp b/src/boost/libs/contract/example/mitchell02/courier.cpp new file mode 100644 index 00000000..e04fa0d9 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/courier.cpp @@ -0,0 +1,207 @@ + +// 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_courier +#include <boost/contract.hpp> +#include <string> +#include <cassert> + +struct package { + double weight_kg; + std::string location; + double accepted_hour; + double delivered_hour; + + explicit package( + double _weight_kg, + std::string const& _location = "", + double _accepted_hour = 0.0, + double _delivered_hour = 0.0 + ) : + weight_kg(_weight_kg), + location(_location), + accepted_hour(_accepted_hour), + delivered_hour(_delivered_hour) + {} +}; + +// Courier for package delivery. +class courier + #define BASES private boost::contract::constructor_precondition<courier> + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + static void static_invariant() { + // Positive min. insurance. + BOOST_CONTRACT_ASSERT(min_insurance_usd >= 0.0); + } + + void invariant() const { + // Above min. insurance. + BOOST_CONTRACT_ASSERT(insurance_cover_usd() >= min_insurance_usd); + } + +public: + static double min_insurance_usd; + + /* Creation */ + + // Create courier with specified insurance value. + explicit courier(double _insurance_cover_usd = min_insurance_usd) : + boost::contract::constructor_precondition<courier>([&] { + // Positive insurance. + BOOST_CONTRACT_ASSERT(_insurance_cover_usd >= 0.0); + }), + insurance_cover_usd_(_insurance_cover_usd) + { + // Check invariants. + boost::contract::check c = boost::contract::constructor(this); + } + + // Destroy courier. + virtual ~courier() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Queries */ + + // Return insurance cover. + double insurance_cover_usd() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return insurance_cover_usd_; + } + + /* Commands */ + + // Deliver package to destination. + virtual void deliver( + package& package_delivery, + std::string const& destination, + boost::contract::virtual_* v = 0 + ) { + boost::contract::check c = boost::contract::public_function(v, this) + .precondition([&] { + // Within max weight of this delivery. + BOOST_CONTRACT_ASSERT(package_delivery.weight_kg < 5.0); + }) + .postcondition([&] { + // Within max delivery type. + BOOST_CONTRACT_ASSERT(double(package_delivery.delivered_hour - + package_delivery.accepted_hour) <= 3.0); + // Delivered at destination. + BOOST_CONTRACT_ASSERT(package_delivery.location == destination); + }) + ; + + package_delivery.location = destination; + // Delivery takes 2.5 hours. + package_delivery.delivered_hour = package_delivery.accepted_hour + 2.5; + } + +private: + double insurance_cover_usd_; +}; + +double courier::min_insurance_usd = 10.0e+6; + +// Different courier for package delivery. +class different_courier + #define BASES private boost::contract::constructor_precondition< \ + different_courier>, public courier + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. + #undef BASES + + static void static_invariant() { + BOOST_CONTRACT_ASSERT( // Better insurance amount. + different_insurance_usd >= courier::min_insurance_usd); + } + + void invariant() const { + // Above different insurance value. + BOOST_CONTRACT_ASSERT(insurance_cover_usd() >= different_insurance_usd); + } + + BOOST_CONTRACT_OVERRIDE(deliver) + +public: + static double different_insurance_usd; + + /* Creation */ + + // Create courier with specified insurance value. + explicit different_courier( + double insurance_cover_usd = different_insurance_usd) : + boost::contract::constructor_precondition<different_courier>([&] { + // Positive insurance value. + BOOST_CONTRACT_ASSERT(insurance_cover_usd > 0.0); + }), + courier(insurance_cover_usd) + { + // Check invariants. + boost::contract::check c = boost::contract::constructor(this); + } + + // Destroy courier. + virtual ~different_courier() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Commands */ + + virtual void deliver( + package& package_delivery, + std::string const& destination, + boost::contract::virtual_* v = 0 + ) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_deliver + >(v, &different_courier::deliver, this, package_delivery, destination) + .precondition([&] { + // Package can weight more (weaker precondition). + BOOST_CONTRACT_ASSERT(package_delivery.weight_kg <= 8.0); + }) + .postcondition([&] { + // Faster delivery (stronger postcondition). + BOOST_CONTRACT_ASSERT(double(package_delivery.delivered_hour - + package_delivery.accepted_hour) <= 2.0); + // Inherited "delivery at destination" postcondition. + }) + ; + + package_delivery.location = destination; + // Delivery takes 0.5 hours. + package_delivery.delivered_hour = package_delivery.accepted_hour + 0.5; + } +}; + +double different_courier::different_insurance_usd = 20.0e+6; + +int main() { + package cups(3.6, "store"); + courier c; + c.deliver(cups, "home"); + assert(cups.location == "home"); + + package desk(7.2, "store"); + different_courier dc; + dc.deliver(desk, "office"); + assert(desk.location == "office"); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/customer_manager.cpp b/src/boost/libs/contract/example/mitchell02/customer_manager.cpp new file mode 100644 index 00000000..1d92120a --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/customer_manager.cpp @@ -0,0 +1,137 @@ + +// 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_customer_manager +#include <boost/contract.hpp> +#include <string> +#include <map> +#include <utility> +#include <cassert> + +// Basic customer information. +struct customer_info { + friend class customer_manager; + + typedef std::string identifier; + + identifier id; + + explicit customer_info(identifier const& _id) : + id(_id), name_(), address_(), birthday_() {} + +private: + std::string name_; + std::string address_; + std::string birthday_; +}; + +// Manage customers. +class customer_manager { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. + } + +public: + /* Creation */ + + customer_manager() { + // Check invariants. + boost::contract::check c = boost::contract::constructor(this); + } + + virtual ~customer_manager() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Basic Queries */ + + int count() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return customers_.size(); + } + + bool id_active(customer_info::identifier const& id) const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return customers_.find(id) != customers_.cend(); + } + + /* Derived Queries */ + + std::string const& name_for(customer_info::identifier const& id) const { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(id_active(id)); // Active. + }) + ; + + // Find != end because of preconditions (no defensive programming). + return customers_.find(id)->second.name_; + } + + /* Commands */ + + void add(customer_info const& info) { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + // Not already active. + BOOST_CONTRACT_ASSERT(!id_active(info.id)); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc. + BOOST_CONTRACT_ASSERT(id_active(info.id)); // Activated. + }) + ; + + customers_.insert(std::make_pair(info.id, customer(info))); + } + + void set_name(customer_info::identifier const& id, + std::string const& name) { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(id_active(id)); // Already active. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(name_for(id) == name); // Name set. + }) + ; + + // Find != end because of precondition (no defensive programming). + customers_.find(id)->second.name_ = name; + } + +private: + class agent {}; // Customer agent. + + struct customer : customer_info { + agent managing_agent; + std::string last_contact; + + explicit customer(customer_info const& info) : customer_info(info), + managing_agent(), last_contact() {} + }; + + std::map<customer_info::identifier, customer> customers_; +}; + +int main() { + customer_manager m; + customer_info const js("john_smith_123"); + m.add(js); + m.set_name(js.id, "John Smith"); + assert(m.name_for(js.id) == "John Smith"); + assert(m.count() == 1); + assert(m.id_active(js.id)); + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/dictionary.cpp b/src/boost/libs/contract/example/mitchell02/dictionary.cpp new file mode 100644 index 00000000..c2731a38 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/dictionary.cpp @@ -0,0 +1,128 @@ + +// 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_dictionary +#include <boost/contract.hpp> +#include <utility> +#include <map> +#include <cassert> + +template<typename K, typename T> +class dictionary { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. + } + +public: + /* Creation */ + + // Create empty dictionary. + dictionary() { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == 0); // Empty. + }) + ; + } + + // Destroy dictionary. + virtual ~dictionary() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Basic Queries */ + + // Number of key entries. + int count() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return items_.size(); + } + + // Has entry for key? + bool has(K const& key) const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Empty has no key. + if(count() == 0) BOOST_CONTRACT_ASSERT(!result); + }) + ; + + return result = (items_.find(key) != items_.end()); + } + + // Value for a given key. + T const& value_for(K const& key) const { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(has(key)); // Has key. + }) + ; + + // Find != end because of precondition (no defensive programming). + return items_.find(key)->second; + } + + /* Commands */ + + // Add value of a given key. + void put(K const& key, T const& value) { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!has(key)); // Has not key already. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc. + BOOST_CONTRACT_ASSERT(has(key)); // Has key. + // Value set for key. + BOOST_CONTRACT_ASSERT(value_for(key) == value); + }) + ; + + items_.insert(std::make_pair(key, value)); + } + + // Remove value for given key. + void remove(K const& key) { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(has(key)); // Has key. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec. + BOOST_CONTRACT_ASSERT(!has(key)); // Has not key. + }) + ; + + items_.erase(key); + } + +private: + std::map<K, T> items_; +}; + +int main() { + std::string const js = "John Smith"; + + dictionary<std::string, int> ages; + assert(!ages.has(js)); + + ages.put(js, 23); + assert(ages.value_for(js) == 23); + + ages.remove(js); + assert(ages.count() == 0); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/name_list.cpp b/src/boost/libs/contract/example/mitchell02/name_list.cpp new file mode 100644 index 00000000..fa394ed5 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/name_list.cpp @@ -0,0 +1,145 @@ + +// 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; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/observer/observer.hpp b/src/boost/libs/contract/example/mitchell02/observer/observer.hpp new file mode 100644 index 00000000..aa8a91ed --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/observer/observer.hpp @@ -0,0 +1,59 @@ + +// 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_observer +#ifndef OBSERVER_HPP_ +#define OBSERVER_HPP_ + +#include <boost/contract.hpp> +#include <cassert> + +// Observer. +class observer { + friend class subject; +public: + // No inv and no bases so contracts optional if no pre, post, and override. + + /* Creation */ + + observer() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::constructor(this); + } + + virtual ~observer() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + /* Commands */ + + // If up-to-date with related subject. + virtual bool up_to_date_with_subject(boost::contract::virtual_* v = 0) + const = 0; + + // Update this observer. + virtual void update(boost::contract::virtual_* v = 0) = 0; +}; + +bool observer::up_to_date_with_subject(boost::contract::virtual_* v) const { + boost::contract::check c = boost::contract::public_function(v, this); + assert(false); + return false; +} + +void observer::update(boost::contract::virtual_* v) { + boost::contract::check c = boost::contract::public_function(v, this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(up_to_date_with_subject()); // Up-to-date. + }) + ; + assert(false); +} + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/observer/subject.hpp b/src/boost/libs/contract/example/mitchell02/observer/subject.hpp new file mode 100644 index 00000000..12aeae71 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/observer/subject.hpp @@ -0,0 +1,165 @@ + +// 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_subject +#ifndef SUBJECT_HPP_ +#define SUBJECT_HPP_ + +#include "observer.hpp" +#include <boost/contract.hpp> +#include <vector> +#include <algorithm> +#include <cassert> + +// Subject for observer design pattern. +class subject { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT_AUDIT(all_observers_valid(observers())); // Valid. + } + +public: + /* Creation */ + + // Construct subject with no observer. + subject() { + // Check invariant. + boost::contract::check c = boost::contract::constructor(this); + } + + // Destroy subject. + virtual ~subject() { + // Check invariant. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Queries */ + + // If given object is attached. + bool attached(observer const* ob) const { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(ob); // Not null. + }) + ; + + return std::find(observers_.cbegin(), observers_.cend(), ob) != + observers_.cend(); + } + + /* Commands */ + + // Attach given object as an observer. + void attach(observer* ob) { + boost::contract::old_ptr<std::vector<observer const*> > old_observers; + #ifdef BOOST_CONTRACT_AUDITS + old_observers = BOOST_CONTRACT_OLDOF(observers()); + #endif + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(ob); // Not null. + BOOST_CONTRACT_ASSERT(!attached(ob)); // Not already attached. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(attached(ob)); // Attached. + // Others not changed (frame rule). + BOOST_CONTRACT_ASSERT_AUDIT(other_observers_unchanged( + *old_observers, observers(), ob)); + }) + ; + + observers_.push_back(ob); + } + +protected: + // Contracts could have been omitted for protected/private with no pre/post. + + /* Queries */ + + // All observers attached to this subject. + std::vector<observer const*> observers() const { + std::vector<observer const*> obs; + for(std::vector<observer*>::const_iterator i = observers_.cbegin(); + i != observers_.cend(); ++i) { + obs.push_back(*i); + } + return obs; + } + + /* Commands */ + + // Update all attached observers. + void notify() { + // Protected members use `function` (no inv and no subcontracting). + boost::contract::check c = boost::contract::function() + .postcondition([&] { + // All updated. + BOOST_CONTRACT_ASSERT_AUDIT(all_observers_updated(observers())); + }) + ; + + for(std::vector<observer*>::iterator i = observers_.begin(); + i != observers_.end(); ++i) { + // Class invariants ensure no null pointers in observers but class + // invariants not checked for non-public functions so assert here. + assert(*i); // Pointer not null (defensive programming). + (*i)->update(); + } + } + +private: + /* Contract Helpers */ + + static bool all_observers_valid(std::vector<observer const*> const& obs) { + for(std::vector<observer const*>::const_iterator i = obs.cbegin(); + i != obs.cend(); ++i) { + if(!*i) return false; + } + return true; + } + + static bool other_observers_unchanged( + std::vector<observer const*> const& old_obs, + std::vector<observer const*> const& new_obs, + observer const* ob + ) { + // Private members use `function` (no inv and no subcontracting). + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(ob); // Not null. + }) + ; + + std::vector<observer const*> remaining = new_obs; + std::remove(remaining.begin(), remaining.end(), ob); + + std::vector<observer const*>::const_iterator remaining_it = + remaining.begin(); + std::vector<observer const*>::const_iterator old_it = old_obs.begin(); + while(remaining.cend() != remaining_it && old_obs.cend() != old_it) { + if(*remaining_it != *old_it) return false; + ++remaining_it; + ++old_it; + } + return true; + } + + static bool all_observers_updated(std::vector<observer const*> const& obs) { + for(std::vector<observer const*>::const_iterator i = obs.cbegin(); + i != obs.cend(); ++i) { + if(!*i) return false; + if(!(*i)->up_to_date_with_subject()) return false; + } + return true; + } + + std::vector<observer*> observers_; +}; + +#endif // #include guard +//] + diff --git a/src/boost/libs/contract/example/mitchell02/observer_main.cpp b/src/boost/libs/contract/example/mitchell02/observer_main.cpp new file mode 100644 index 00000000..0f6c1a5b --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/observer_main.cpp @@ -0,0 +1,118 @@ + +// 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_observer_main +#include "observer/observer.hpp" +#include "observer/subject.hpp" +#include <boost/contract.hpp> +#include <cassert> + +int test_state; // For testing only. + +// Implement an actual subject. +class concrete_subject + #define BASES public subject + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. + #undef BASES + +public: + typedef int state; // Some state being observed. + + concrete_subject() : state_() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::constructor(this); + } + + virtual ~concrete_subject() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + void set_state(state const& new_state) { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::public_function(this); + + state_ = new_state; + assert(state_ == test_state); + notify(); // Notify all observers. + } + + state get_state() const { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::public_function(this); + return state_; + } + +private: + state state_; +}; + +// Implement an actual observer. +class concrete_observer + #define BASES public observer + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. + #undef BASES + + BOOST_CONTRACT_OVERRIDES(up_to_date_with_subject, update) + +public: + // Create concrete observer. + explicit concrete_observer(concrete_subject const& subj) : + subject_(subj), observed_state_() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::constructor(this); + } + + virtual ~concrete_observer() { + // Could have omitted contracts here (nothing to check). + boost::contract::check c = boost::contract::destructor(this); + } + + // Implement base virtual functions. + + bool up_to_date_with_subject(boost::contract::virtual_* v = 0) + const /* override */ { + bool result; + boost::contract::check c = boost::contract::public_function< + override_up_to_date_with_subject + >(v, result, &concrete_observer::up_to_date_with_subject, this); + + return result = true; // For simplicity, assume always up-to-date. + } + + void update(boost::contract::virtual_* v = 0) /* override */ { + boost::contract::check c = boost::contract::public_function< + override_update>(v, &concrete_observer::update, this); + + observed_state_ = subject_.get_state(); + assert(observed_state_ == test_state); + } + +private: + concrete_subject const& subject_; + concrete_subject::state observed_state_; +}; + +int main() { + concrete_subject subj; + concrete_observer ob(subj); + subj.attach(&ob); + + subj.set_state(test_state = 123); + subj.set_state(test_state = 456); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/simple_queue.cpp b/src/boost/libs/contract/example/mitchell02/simple_queue.cpp new file mode 100644 index 00000000..e0250137 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/simple_queue.cpp @@ -0,0 +1,219 @@ + +// 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_simple_queue +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <vector> +#include <cassert> + +template<typename T> +class simple_queue + #define BASES private boost::contract::constructor_precondition< \ + simple_queue<T> > + : BASES +{ + friend class boost::contract::access; + + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; + #undef BASES + + void invariant() const { + BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. + } + +public: + /* Creation */ + + // Create empty queue. + explicit simple_queue(int a_capacity) : + boost::contract::constructor_precondition<simple_queue>([&] { + BOOST_CONTRACT_ASSERT(a_capacity > 0); // Positive capacity. + }) + { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + // Capacity set. + BOOST_CONTRACT_ASSERT(capacity() == a_capacity); + BOOST_CONTRACT_ASSERT(is_empty()); // Empty. + }) + ; + + items_.reserve(a_capacity); + } + + // Destroy queue. + virtual ~simple_queue() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Basic Queries */ + + // Items in queue (in their order). + // (Somewhat exposes implementation but allows to check more contracts.) + std::vector<T> const& items() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return items_; + } + + // Max number of items queue can hold. + int capacity() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return items_.capacity(); + } + + /* Derived Queries */ + + // Number of items. + int count() const { + int result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Return items count. + BOOST_CONTRACT_ASSERT(result == int(items().size())); + }) + ; + + return result = items_.size(); + } + + // Item at head. + T const& head() const { + boost::optional<T const&> result; + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!is_empty()); // Not empty. + }) + .postcondition([&] { + // Return item on top. + BOOST_CONTRACT_ASSERT(*result == items().at(0)); + }) + ; + + return *(result = items_.at(0)); + } + + // If queue contains no item. + bool is_empty() const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Consistent with count. + BOOST_CONTRACT_ASSERT(result == (count() == 0)); + }) + ; + + return result = (items_.size() == 0); + } + + // If queue has no room for another item. + bool is_full() const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT( // Consistent with size and capacity. + result == (capacity() == int(items().size()))); + }) + ; + + return result = (items_.size() == items_.capacity()); + } + + /* Commands */ + + // Remove head itme and shift all other items. + void remove() { + // Expensive all_equal postcond. and old_items copy might be skipped. + boost::contract::old_ptr<std::vector<T> > old_items; + #ifdef BOOST_CONTRACT_AUDIITS + = BOOST_CONTRACT_OLDOF(items()) + #endif // Else, leave old pointer null... + ; + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(!is_empty()); // Not empty. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec. + // ...following skipped #ifndef AUDITS. + if(old_items) all_equal(items(), *old_items, /* shifted = */ 1); + }) + ; + + items_.erase(items_.begin()); + } + + // Add item to tail. + void put(T const& item) { + // Expensive all_equal postcond. and old_items copy might be skipped. + boost::contract::old_ptr<std::vector<T> > old_items; + #ifdef BOOST_CONTRACT_AUDITS + = BOOST_CONTRACT_OLDOF(items()) + #endif // Else, leave old pointer null... + ; + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(count() < capacity()); // Room for add. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc. + // Second to last item. + BOOST_CONTRACT_ASSERT(items().at(count() - 1) == item); + // ...following skipped #ifndef AUDITS. + if(old_items) all_equal(items(), *old_items); + }) + ; + + items_.push_back(item); + } + +private: + // Contract helper. + static bool all_equal(std::vector<T> const& left, + std::vector<T> const& right, unsigned offset = 0) { + boost::contract::check c = boost::contract::function() + .precondition([&] { + // Correct offset. + BOOST_CONTRACT_ASSERT(right.size() == left.size() + offset); + }) + ; + + for(unsigned i = offset; i < right.size(); ++i) { + if(left.at(i - offset) != right.at(i)) return false; + } + return true; + } + + std::vector<T> items_; +}; + +int main() { + simple_queue<int> q(10); + q.put(123); + q.put(456); + + assert(q.capacity() == 10); + assert(q.head() == 123); + + assert(!q.is_empty()); + assert(!q.is_full()); + + std::vector<int> const& items = q.items(); + assert(items.at(0) == 123); + assert(items.at(1) == 456); + + q.remove(); + assert(q.count() == 1); + + return 0; +} +//] + diff --git a/src/boost/libs/contract/example/mitchell02/stack.cpp b/src/boost/libs/contract/example/mitchell02/stack.cpp new file mode 100644 index 00000000..a0bd6b14 --- /dev/null +++ b/src/boost/libs/contract/example/mitchell02/stack.cpp @@ -0,0 +1,138 @@ + +// 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_stack +#include <boost/contract.hpp> +#include <boost/optional.hpp> +#include <vector> +#include <cassert> + +template<typename T> +class stack { + friend class boost::contract::access; + + void invariant() const { + BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count. + } + +public: + /* Creation */ + + // Create empty stack. + stack() { + boost::contract::check c = boost::contract::constructor(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == 0); // Empty. + }) + ; + } + + // Destroy stack. + virtual ~stack() { + // Check invariants. + boost::contract::check c = boost::contract::destructor(this); + } + + /* Basic Queries */ + + // Number of items. + int count() const { + // Check invariants. + boost::contract::check c = boost::contract::public_function(this); + return items_.size(); + } + + // Item at index in [1, count()] (as in Eiffel). + T const& item_at(int index) const { + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(index > 0); // Positive index. + BOOST_CONTRACT_ASSERT(index <= count()); // Index within count. + }) + ; + + return items_[index - 1]; + } + + /* Derived Queries */ + + // If no items. + bool is_empty() const { + bool result; + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + // Consistent with count. + BOOST_CONTRACT_ASSERT(result == (count() == 0)); + }) + ; + + return result = (count() == 0); + } + + // Top item. + T const& item() const { + boost::optional<T const&> result; // Avoid extra construction of T. + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(count() > 0); // Not empty. + }) + .postcondition([&] { + // Item on top. + BOOST_CONTRACT_ASSERT(*result == item_at(count())); + }) + ; + + return *(result = item_at(count())); + } + + /* Commands */ + + // Push item to the top. + void put(T const& new_item) { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc. + BOOST_CONTRACT_ASSERT(item() == new_item); // Item set. + }) + ; + + items_.push_back(new_item); + } + + // Pop top item. + void remove() { + boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count()); + boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(count() > 0); // Not empty. + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec. + }) + ; + + items_.pop_back(); + } + +private: + std::vector<T> items_; +}; + +int main() { + stack<int> s; + assert(s.count() == 0); + + s.put(123); + assert(s.item() == 123); + + s.remove(); + assert(s.is_empty()); + + return 0; +} +//] + |