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_name_list
8 #include <boost/contract.hpp>
9 #include <string>
10 #include <vector>
11 #include <algorithm>
12 #include <cassert>
13
14 // List of names.
15 class name_list {
16 friend class boost::contract::access;
17
invariant() const18 void invariant() const {
19 BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
20 }
21
22 public:
23 /* Creation */
24
25 // Create an empty list.
name_list()26 name_list() {
27 boost::contract::check c = boost::contract::constructor(this)
28 .postcondition([&] {
29 BOOST_CONTRACT_ASSERT(count() == 0); // Empty list.
30 })
31 ;
32 }
33
34 // Destroy list.
~name_list()35 virtual ~name_list() {
36 // Check invariants.
37 boost::contract::check c = boost::contract::destructor(this);
38 }
39
40 /* Basic Queries */
41
42 // Number of names in list.
count() const43 int count() const {
44 // Check invariants.
45 boost::contract::check c = boost::contract::public_function(this);
46 return names_.size();
47 }
48
49 // Is name in list?
has(std::string const & name) const50 bool has(std::string const& name) const {
51 bool result;
52 boost::contract::check c = boost::contract::public_function(this)
53 .postcondition([&] {
54 // If empty, has not.
55 if(count() == 0) BOOST_CONTRACT_ASSERT(!result);
56 })
57 ;
58
59 return result = names_.cend() != std::find(names_.cbegin(),
60 names_.cend(), name);
61 }
62
63 /* Commands */
64
65 // Add name to list, if name not already in list.
put(std::string const & name,boost::contract::virtual_ * v=0)66 virtual void put(std::string const& name,
67 boost::contract::virtual_* v = 0) {
68 boost::contract::old_ptr<bool> old_has_name =
69 BOOST_CONTRACT_OLDOF(v, has(name));
70 boost::contract::old_ptr<int> old_count =
71 BOOST_CONTRACT_OLDOF(v, count());
72 boost::contract::check c = boost::contract::public_function(v, this)
73 .precondition([&] {
74 BOOST_CONTRACT_ASSERT(!has(name)); // Not already in list.
75 })
76 .postcondition([&] {
77 if(!*old_has_name) { // If-guard allows to relax subcontracts.
78 BOOST_CONTRACT_ASSERT(has(name)); // Name in list.
79 BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Inc.
80 }
81 })
82 ;
83
84 names_.push_back(name);
85 }
86
87 private:
88 std::vector<std::string> names_;
89 };
90
91 class relaxed_name_list
92 #define BASES public name_list
93 : BASES
94 {
95 friend class boost::contract::access;
96
97 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting.
98 #undef BASES
99
100 BOOST_CONTRACT_OVERRIDE(put);
101
102 public:
103 /* Commands */
104
105 // Add name to list, or do nothing if name already in list (relaxed).
put(std::string const & name,boost::contract::virtual_ * v=0)106 void put(std::string const& name,
107 boost::contract::virtual_* v = 0) /* override */ {
108 boost::contract::old_ptr<bool> old_has_name =
109 BOOST_CONTRACT_OLDOF(v, has(name));
110 boost::contract::old_ptr<int> old_count =
111 BOOST_CONTRACT_OLDOF(v, count());
112 boost::contract::check c = boost::contract::public_function<
113 override_put>(v, &relaxed_name_list::put, this, name)
114 .precondition([&] { // Relax inherited preconditions.
115 BOOST_CONTRACT_ASSERT(has(name)); // Already in list.
116 })
117 .postcondition([&] { // Inherited post. not checked given if-guard.
118 if(*old_has_name) {
119 // Count unchanged if name already in list.
120 BOOST_CONTRACT_ASSERT(count() == *old_count);
121 }
122 })
123 ;
124
125 if(!has(name)) name_list::put(name); // Else, do nothing.
126 }
127 };
128
main()129 int main() {
130 std::string const js = "John Smith";
131
132 relaxed_name_list rl;
133 rl.put(js);
134 assert(rl.has(js));
135 rl.put(js); // OK, relaxed contracts allow calling this again (do nothing).
136
137 name_list nl;
138 nl.put(js);
139 assert(nl.has(js));
140 // nl.put(js); // Error, contracts do not allow calling this again.
141
142 return 0;
143 }
144 //]
145
146