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.
15struct customer_info {
16 friend class customer_manager;
17
18 typedef std::string identifier;
19
20 identifier id;
21
22 explicit customer_info(identifier const& _id) :
23 id(_id), name_(), address_(), birthday_() {}
24
25private:
26 std::string name_;
27 std::string address_;
28 std::string birthday_;
29};
30
31// Manage customers.
32class customer_manager {
33 friend class boost::contract::access;
34
35 void invariant() const {
36 BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
37 }
38
39public:
40 /* Creation */
41
42 customer_manager() {
43 // Check invariants.
44 boost::contract::check c = boost::contract::constructor(obj: this);
45 }
46
47 virtual ~customer_manager() {
48 // Check invariants.
49 boost::contract::check c = boost::contract::destructor(obj: this);
50 }
51
52 /* Basic Queries */
53
54 int count() const {
55 // Check invariants.
56 boost::contract::check c = boost::contract::public_function(obj: this);
57 return customers_.size();
58 }
59
60 bool id_active(customer_info::identifier const& id) const {
61 // Check invariants.
62 boost::contract::check c = boost::contract::public_function(obj: this);
63 return customers_.find(x: id) != customers_.cend();
64 }
65
66 /* Derived Queries */
67
68 std::string const& name_for(customer_info::identifier const& id) const {
69 boost::contract::check c = boost::contract::public_function(obj: this)
70 .precondition(f: [&] {
71 BOOST_CONTRACT_ASSERT(id_active(id)); // Active.
72 })
73 ;
74
75 // Find != end because of preconditions (no defensive programming).
76 return customers_.find(x: id)->second.name_;
77 }
78
79 /* Commands */
80
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(obj: this)
84 .precondition(f: [&] {
85 // Not already active.
86 BOOST_CONTRACT_ASSERT(!id_active(info.id));
87 })
88 .postcondition(f: [&] {
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(x: std::make_pair(x: info.id, y: customer(info)));
95 }
96
97 void set_name(customer_info::identifier const& id,
98 std::string const& name) {
99 boost::contract::check c = boost::contract::public_function(obj: this)
100 .precondition(f: [&] {
101 BOOST_CONTRACT_ASSERT(id_active(id)); // Already active.
102 })
103 .postcondition(f: [&] {
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(x: id)->second.name_ = name;
110 }
111
112private:
113 class agent {}; // Customer agent.
114
115 struct customer : customer_info {
116 agent managing_agent;
117 std::string last_contact;
118
119 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
126int main() {
127 customer_manager m;
128 customer_info const js("john_smith_123");
129 m.add(info: js);
130 m.set_name(id: js.id, name: "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

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