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 #include <boost/contract.hpp>
8 #include <limits>
9 #include <cassert>
10
11 //[private_protected_virtual_counter
12 class counter {
13 // Virtual private and protected functions still declare extra
14 // `virtual_* = 0` parameter (otherwise they cannot be overridden), but...
15 protected:
set(int n,boost::contract::virtual_ * =0)16 virtual void set(int n, boost::contract::virtual_* = 0) {
17 boost::contract::check c = boost::contract::function() // ...no `v`.
18 .precondition([&] {
19 BOOST_CONTRACT_ASSERT(n <= 0);
20 })
21 .postcondition([&] {
22 BOOST_CONTRACT_ASSERT(get() == n);
23 })
24 ;
25
26 n_ = n;
27 }
28
29 private:
dec(boost::contract::virtual_ * =0)30 virtual void dec(boost::contract::virtual_* = 0) {
31 boost::contract::old_ptr<int> old_get = BOOST_CONTRACT_OLDOF(get()); // ...no `v`.
32 boost::contract::check c = boost::contract::function() // ...no `v`.
33 .precondition([&] {
34 BOOST_CONTRACT_ASSERT(
35 get() + 1 >= std::numeric_limits<int>::min());
36 })
37 .postcondition([&] {
38 BOOST_CONTRACT_ASSERT(get() == *old_get - 1);
39 })
40 ;
41
42 set(get() - 1);
43 }
44
45 int n_;
46
47 /* ... */
48 //]
49
50 public:
get(boost::contract::virtual_ * v=0) const51 virtual int get(boost::contract::virtual_* v = 0) const {
52 int result;
53 boost::contract::check c = boost::contract::public_function(
54 v, result, this)
55 .postcondition([&] (int const result) {
56 BOOST_CONTRACT_ASSERT(result <= 0);
57 BOOST_CONTRACT_ASSERT(result == n_);
58 })
59 ;
60
61 return result = n_;
62 }
63
counter()64 counter() : n_(0) {} // Should contract constructor and destructor too.
65
invariant() const66 void invariant() const {
67 BOOST_CONTRACT_ASSERT(get() <= 0);
68 }
69
70 friend int main();
71 };
72
73 //[private_protected_virtual_counter10
74 class counter10
75 #define BASES public counter
76 : BASES
77 {
78 public:
79 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
80 #undef BASES
81
82 // Overriding from non-public members so no subcontracting, no override_...
83
set(int n,boost::contract::virtual_ * v=0)84 virtual void set(int n, boost::contract::virtual_* v = 0) /* override */ {
85 boost::contract::check c = boost::contract::public_function(v, this)
86 .precondition([&] {
87 BOOST_CONTRACT_ASSERT(n % 10 == 0);
88 })
89 .postcondition([&] {
90 BOOST_CONTRACT_ASSERT(get() == n);
91 })
92 ;
93
94 counter::set(n);
95 }
96
dec(boost::contract::virtual_ * v=0)97 virtual void dec(boost::contract::virtual_* v = 0) /* override */ {
98 boost::contract::old_ptr<int> old_get = BOOST_CONTRACT_OLDOF(v, get());
99 boost::contract::check c = boost::contract::public_function(v, this)
100 .precondition([&] {
101 BOOST_CONTRACT_ASSERT(
102 get() + 10 >= std::numeric_limits<int>::min());
103 })
104 .postcondition([&] {
105 BOOST_CONTRACT_ASSERT(get() == *old_get - 10);
106 })
107 ;
108
109 set(get() - 10);
110 }
111
112 /* ... */
113 //]
114
get(boost::contract::virtual_ * v=0) const115 virtual int get(boost::contract::virtual_* v = 0) const {
116 int result;
117 boost::contract::check c = boost::contract::public_function<
118 override_get>(v, result, &counter10::get, this);
119
120 return result = counter::get();
121 }
BOOST_CONTRACT_OVERRIDE(get)122 BOOST_CONTRACT_OVERRIDE(get)
123
124 // Should contract default constructor and destructor too.
125
126 void invariant() const {
127 BOOST_CONTRACT_ASSERT(get() % 10 == 0);
128 }
129 };
130
main()131 int main() {
132 counter cnt;
133 assert(cnt.get() == 0);
134 cnt.dec();
135 assert(cnt.get() == -1);
136
137 counter10 cnt10;
138 counter& b = cnt10; // Polymorphic calls.
139 assert(b.get() == 0);
140 b.dec();
141 assert(b.get() == -10);
142
143 return 0;
144 }
145
146