diff options
author | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-04-21 11:54:28 +0000 |
---|---|---|
committer | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-04-21 11:54:28 +0000 |
commit | e6918187568dbd01842d8d1d2c808ce16a894239 (patch) | |
tree | 64f88b554b444a49f656b6c656111a145cbbaa28 /src/boost/libs/contract/example/mitchell02/dictionary.cpp | |
parent | Initial commit. (diff) | |
download | ceph-e6918187568dbd01842d8d1d2c808ce16a894239.tar.xz ceph-e6918187568dbd01842d8d1d2c808ce16a894239.zip |
Adding upstream version 18.2.2.upstream/18.2.2
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'src/boost/libs/contract/example/mitchell02/dictionary.cpp')
-rw-r--r-- | src/boost/libs/contract/example/mitchell02/dictionary.cpp | 128 |
1 files changed, 128 insertions, 0 deletions
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 000000000..c2731a38f --- /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; +} +//] + |