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 <vector>
8 #include <limits>
9 #include <cassert>
10
11 //[ifdef_macro_function
12 // Use macro interface to completely disable contract code compilation.
13 #include <boost/contract_macro.hpp>
14
inc(int & x)15 int inc(int& x) {
16 int result;
17 BOOST_CONTRACT_OLD_PTR(int)(old_x, x);
18 BOOST_CONTRACT_FUNCTION()
19 BOOST_CONTRACT_PRECONDITION([&] {
20 BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max());
21 })
22 BOOST_CONTRACT_POSTCONDITION([&] {
23 BOOST_CONTRACT_ASSERT(x == *old_x + 1);
24 BOOST_CONTRACT_ASSERT(result == *old_x);
25 })
26 ;
27
28 return result = x++;
29 }
30 //]
31
32 template<typename T>
33 class pushable {
34 friend class boost::contract::access; // Left in code (almost no overhead).
35
36 BOOST_CONTRACT_INVARIANT({
37 BOOST_CONTRACT_ASSERT(capacity() <= max_size());
38 })
39
40 public:
41 virtual void push_back(
42 T const& x,
43 boost::contract::virtual_* v = 0 // Left in code (almost no overhead).
44 ) = 0;
45
46 protected:
47 virtual unsigned capacity() const = 0;
48 virtual unsigned max_size() const = 0;
49 };
50
51 template<typename T>
push_back(T const & x,boost::contract::virtual_ * v)52 void pushable<T>::push_back(T const& x, boost::contract::virtual_* v) {
53 BOOST_CONTRACT_OLD_PTR(unsigned)(v, old_capacity, capacity());
54 BOOST_CONTRACT_PUBLIC_FUNCTION(v, this)
55 BOOST_CONTRACT_PRECONDITION([&] {
56 BOOST_CONTRACT_ASSERT(capacity() < max_size());
57 })
58 BOOST_CONTRACT_POSTCONDITION([&] {
59 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
60 })
61 ;
62 assert(false); // Shall never execute this body.
63 }
64
65 //[ifdef_macro_class
66 class integers
67 #define BASES public pushable<int>
68 :
69 // Left in code (almost no overhead).
70 private boost::contract::constructor_precondition<integers>,
71 BASES
72 {
73 // Followings left in code (almost no overhead).
74 friend class boost::contract::access;
75
76 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
77 #undef BASES
78
79 BOOST_CONTRACT_INVARIANT({
80 BOOST_CONTRACT_ASSERT(size() <= capacity());
81 })
82
83 public:
integers(int from,int to)84 integers(int from, int to) :
85 BOOST_CONTRACT_CONSTRUCTOR_PRECONDITION(integers)([&] {
86 BOOST_CONTRACT_ASSERT(from <= to);
87 }),
88 vect_(to - from + 1)
89 {
90 BOOST_CONTRACT_CONSTRUCTOR(this)
__anon8b6d42090602null91 BOOST_CONTRACT_POSTCONDITION([&] {
92 BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1));
93 })
94 ;
95
96 for(int x = from; x <= to; ++x) vect_.at(x - from) = x;
97 }
98
~integers()99 virtual ~integers() {
100 BOOST_CONTRACT_DESTRUCTOR(this); // Check invariants.
101 }
102
push_back(int const & x,boost::contract::virtual_ * v=0)103 virtual void push_back(
104 int const& x,
105 boost::contract::virtual_* v = 0 // Left in code (almost no overhead).
106 ) /* override */ {
107 BOOST_CONTRACT_OLD_PTR(unsigned)(old_size);
108 BOOST_CONTRACT_PUBLIC_FUNCTION_OVERRIDE(override_push_back)(
109 v, &integers::push_back, this, x)
110 BOOST_CONTRACT_PRECONDITION([&] {
111 BOOST_CONTRACT_ASSERT(size() < max_size());
112 })
113 BOOST_CONTRACT_OLD([&] {
114 old_size = BOOST_CONTRACT_OLDOF(v, size());
115 })
116 BOOST_CONTRACT_POSTCONDITION([&] {
117 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
118 })
119 BOOST_CONTRACT_EXCEPT([&] {
120 BOOST_CONTRACT_ASSERT(size() == *old_size);
121 })
122 ;
123
124 vect_.push_back(x);
125 }
126
127 private:
128 BOOST_CONTRACT_OVERRIDE(push_back) // Left in code (almost no overhead).
129
130 /* ... */
131 //]
132
133 public: // Could program contracts for these too...
size() const134 unsigned size() const { return vect_.size(); }
max_size() const135 unsigned max_size() const { return vect_.max_size(); }
capacity() const136 unsigned capacity() const { return vect_.capacity(); }
137
138 private:
139 std::vector<int> vect_;
140 };
141
main()142 int main() {
143 integers i(1, 10);
144 int x = 123;
145 i.push_back(inc(x));
146 assert(x == 124);
147 assert(i.size() == 11);
148 return 0;
149 }
150
151