1
2// Copyright (C) 2008-2018 Lorenzo Caminiti
3// Distributed under the Boost Software License, Version 1.0 (see accompanying
4// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
5// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
6
7//[mitchell02_dictionary
8#include <boost/contract.hpp>
9#include <utility>
10#include <map>
11#include <cassert>
12
13template<typename K, typename T>
14class dictionary {
15 friend class boost::contract::access;
16
17 void invariant() const {
18 BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
19 }
20
21public:
22 /* Creation */
23
24 // Create empty dictionary.
25 dictionary() {
26 boost::contract::check c = boost::contract::constructor(this)
27 .postcondition([&] {
28 BOOST_CONTRACT_ASSERT(count() == 0); // Empty.
29 })
30 ;
31 }
32
33 // Destroy dictionary.
34 virtual ~dictionary() {
35 // Check invariants.
36 boost::contract::check c = boost::contract::destructor(this);
37 }
38
39 /* Basic Queries */
40
41 // Number of key entries.
42 int count() const {
43 // Check invariants.
44 boost::contract::check c = boost::contract::public_function(this);
45 return items_.size();
46 }
47
48 // Has entry for key?
49 bool has(K const& key) const {
50 bool result;
51 boost::contract::check c = boost::contract::public_function(this)
52 .postcondition([&] {
53 // Empty has no key.
54 if(count() == 0) BOOST_CONTRACT_ASSERT(!result);
55 })
56 ;
57
58 return result = (items_.find(key) != items_.end());
59 }
60
61 // Value for a given key.
62 T const& value_for(K const& key) const {
63 boost::contract::check c = boost::contract::public_function(this)
64 .precondition([&] {
65 BOOST_CONTRACT_ASSERT(has(key)); // Has key.
66 })
67 ;
68
69 // Find != end because of precondition (no defensive programming).
70 return items_.find(key)->second;
71 }
72
73 /* Commands */
74
75 // Add value of a given key.
76 void put(K const& key, T const& value) {
77 boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
78 boost::contract::check c = boost::contract::public_function(this)
79 .precondition([&] {
80 BOOST_CONTRACT_ASSERT(!has(key)); // Has not key already.
81 })
82 .postcondition([&] {
83 BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc.
84 BOOST_CONTRACT_ASSERT(has(key)); // Has key.
85 // Value set for key.
86 BOOST_CONTRACT_ASSERT(value_for(key) == value);
87 })
88 ;
89
90 items_.insert(std::make_pair(key, value));
91 }
92
93 // Remove value for given key.
94 void remove(K const& key) {
95 boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
96 boost::contract::check c = boost::contract::public_function(this)
97 .precondition([&] {
98 BOOST_CONTRACT_ASSERT(has(key)); // Has key.
99 })
100 .postcondition([&] {
101 BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec.
102 BOOST_CONTRACT_ASSERT(!has(key)); // Has not key.
103 })
104 ;
105
106 items_.erase(key);
107 }
108
109private:
110 std::map<K, T> items_;
111};
112
113int main() {
114 std::string const js = "John Smith";
115
116 dictionary<std::string, int> ages;
117 assert(!ages.has(js));
118
119 ages.put(key: js, value: 23);
120 assert(ages.value_for(js) == 23);
121
122 ages.remove(key: js);
123 assert(ages.count() == 0);
124
125 return 0;
126}
127//]
128
129

source code of boost/libs/contract/example/mitchell02/dictionary.cpp