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