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_customer_manager
8 #include <boost/contract.hpp>
9 #include <string>
10 #include <map>
11 #include <utility>
12 #include <cassert>
13
14 // Basic customer information.
15 struct customer_info {
16 friend class customer_manager;
17
18 typedef std::string identifier;
19
20 identifier id;
21
customer_infocustomer_info22 explicit customer_info(identifier const& _id) :
23 id(_id), name_(), address_(), birthday_() {}
24
25 private:
26 std::string name_;
27 std::string address_;
28 std::string birthday_;
29 };
30
31 // Manage customers.
32 class customer_manager {
33 friend class boost::contract::access;
34
invariant() const35 void invariant() const {
36 BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
37 }
38
39 public:
40 /* Creation */
41
customer_manager()42 customer_manager() {
43 // Check invariants.
44 boost::contract::check c = boost::contract::constructor(this);
45 }
46
~customer_manager()47 virtual ~customer_manager() {
48 // Check invariants.
49 boost::contract::check c = boost::contract::destructor(this);
50 }
51
52 /* Basic Queries */
53
count() const54 int count() const {
55 // Check invariants.
56 boost::contract::check c = boost::contract::public_function(this);
57 return customers_.size();
58 }
59
id_active(customer_info::identifier const & id) const60 bool id_active(customer_info::identifier const& id) const {
61 // Check invariants.
62 boost::contract::check c = boost::contract::public_function(this);
63 return customers_.find(id) != customers_.cend();
64 }
65
66 /* Derived Queries */
67
name_for(customer_info::identifier const & id) const68 std::string const& name_for(customer_info::identifier const& id) const {
69 boost::contract::check c = boost::contract::public_function(this)
70 .precondition([&] {
71 BOOST_CONTRACT_ASSERT(id_active(id)); // Active.
72 })
73 ;
74
75 // Find != end because of preconditions (no defensive programming).
76 return customers_.find(id)->second.name_;
77 }
78
79 /* Commands */
80
add(customer_info const & info)81 void add(customer_info const& info) {
82 boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
83 boost::contract::check c = boost::contract::public_function(this)
84 .precondition([&] {
85 // Not already active.
86 BOOST_CONTRACT_ASSERT(!id_active(info.id));
87 })
88 .postcondition([&] {
89 BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc.
90 BOOST_CONTRACT_ASSERT(id_active(info.id)); // Activated.
91 })
92 ;
93
94 customers_.insert(std::make_pair(info.id, customer(info)));
95 }
96
set_name(customer_info::identifier const & id,std::string const & name)97 void set_name(customer_info::identifier const& id,
98 std::string const& name) {
99 boost::contract::check c = boost::contract::public_function(this)
100 .precondition([&] {
101 BOOST_CONTRACT_ASSERT(id_active(id)); // Already active.
102 })
103 .postcondition([&] {
104 BOOST_CONTRACT_ASSERT(name_for(id) == name); // Name set.
105 })
106 ;
107
108 // Find != end because of precondition (no defensive programming).
109 customers_.find(id)->second.name_ = name;
110 }
111
112 private:
113 class agent {}; // Customer agent.
114
115 struct customer : customer_info {
116 agent managing_agent;
117 std::string last_contact;
118
customercustomer_manager::customer119 explicit customer(customer_info const& info) : customer_info(info),
120 managing_agent(), last_contact() {}
121 };
122
123 std::map<customer_info::identifier, customer> customers_;
124 };
125
main()126 int main() {
127 customer_manager m;
128 customer_info const js("john_smith_123");
129 m.add(js);
130 m.set_name(js.id, "John Smith");
131 assert(m.name_for(js.id) == "John Smith");
132 assert(m.count() == 1);
133 assert(m.id_active(js.id));
134 return 0;
135 }
136 //]
137
138