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 <vector>
9 #include <cassert>
10
11 template<typename T>
12 class pushable {
13 friend class boost::contract::access;
14
invariant() const15 void invariant() const {
16 BOOST_CONTRACT_ASSERT(capacity() <= max_size());
17 }
18
19 public:
20 virtual void push_back(T const& value, boost::contract::virtual_* v = 0)
21 = 0;
22
23 protected:
24 virtual unsigned capacity() const = 0;
25 virtual unsigned max_size() const = 0;
26 };
27
28 template<typename T>
push_back(T const & value,boost::contract::virtual_ * v)29 void pushable<T>::push_back(T const& value, boost::contract::virtual_* v) {
30 boost::contract::old_ptr<unsigned> old_capacity =
31 BOOST_CONTRACT_OLDOF(v, capacity());
32 boost::contract::check c = boost::contract::public_function(v, this)
33 .precondition([&] {
34 BOOST_CONTRACT_ASSERT(capacity() < max_size());
35 })
36 .postcondition([&] {
37 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
38 })
39 ;
40 assert(false);
41 }
42
43 //[access
44 template<typename T>
45 class vector
46 #define BASES public pushable<T>
47 : BASES
48 { // Private section of the class.
49 friend class boost::contract::access; // Friend `access` class so...
50
51 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // ...private bases.
52 #undef BASES
53
invariant() const54 void invariant() const { // ...private invariants.
55 BOOST_CONTRACT_ASSERT(size() <= capacity());
56 }
57
58 BOOST_CONTRACT_OVERRIDE(push_back) // ...private overrides.
59
60 public: // Public section of the class.
push_back(T const & value,boost::contract::virtual_ * v=0)61 void push_back(T const& value, boost::contract::virtual_* v = 0)
62 /* override */ {
63 boost::contract::old_ptr<unsigned> old_size =
64 BOOST_CONTRACT_OLDOF(v, size());
65 boost::contract::check c = boost::contract::public_function<
66 override_push_back>(v, &vector::push_back, this, value)
67 .precondition([&] {
68 BOOST_CONTRACT_ASSERT(size() < max_size());
69 })
70 .postcondition([&] {
71 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
72 })
73 ;
74
75 vect_.push_back(value);
76 }
77
78 /* ... */
79 //]
80
size() const81 unsigned size() const { return vect_.size(); }
max_size() const82 unsigned max_size() const { return vect_.max_size(); }
capacity() const83 unsigned capacity() const { return vect_.capacity(); }
84
85 private: // Another private section.
86 std::vector<T> vect_;
87 };
88
main()89 int main() {
90 vector<int> vect;
91 vect.push_back(123);
92 assert(vect.size() == 1);
93 return 0;
94 }
95
96