• Home
  • Line#
  • Scopes#
  • Navigate#
  • Raw
  • Download
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 
13 template<typename K, typename T>
14 class dictionary {
15     friend class boost::contract::access;
16 
invariant() const17     void invariant() const {
18         BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
19     }
20 
21 public:
22     /* Creation */
23 
24     // Create empty dictionary.
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.
~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.
count() const42     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?
has(K const & key) const49     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.
value_for(K const & key) const62     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.
put(K const & key,T const & value)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.
remove(K const & 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 
109 private:
110     std::map<K, T> items_;
111 };
112 
main()113 int main() {
114     std::string const js = "John Smith";
115 
116     dictionary<std::string, int> ages;
117     assert(!ages.has(js));
118 
119     ages.put(js, 23);
120     assert(ages.value_for(js) == 23);
121 
122     ages.remove(js);
123     assert(ages.count() == 0);
124 
125     return 0;
126 }
127 //]
128 
129