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 { // Somewhat arbitrary base (used just to show subcontracting).
13 public:
invariant() const14 void invariant() const {
15 BOOST_CONTRACT_ASSERT(capacity() <= max_size());
16 }
17
18 virtual void push_back(T const& value,
19 boost::contract::virtual_* v = 0) = 0; // Pure virtual function.
20
21 protected:
22 virtual unsigned capacity() const = 0;
23 virtual unsigned max_size() const = 0;
24 };
25
26 template<typename T> // Contract for pure virtual function.
push_back(T const & value,boost::contract::virtual_ * v)27 void pushable<T>::push_back(T const& value, boost::contract::virtual_* v) {
28 boost::contract::old_ptr<unsigned> old_capacity =
29 BOOST_CONTRACT_OLDOF(v, capacity());
30 boost::contract::check c = boost::contract::public_function(v, this)
31 .precondition([&] {
32 BOOST_CONTRACT_ASSERT(capacity() < max_size());
33 })
34 .postcondition([&] {
35 BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
36 })
37 ;
38 assert(false); // Shall never execute this body.
39 }
40
41 //[introduction_public
42 template<typename T>
43 class vector
44 #define BASES public pushable<T>
45 : BASES
46 {
47 public:
48 typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // For subcontracting.
49 #undef BASES
50
invariant() const51 void invariant() const { // Checked in AND with base class invariants.
52 BOOST_CONTRACT_ASSERT(size() <= capacity());
53 }
54
push_back(T const & value,boost::contract::virtual_ * v=0)55 virtual void push_back(T const& value,
56 boost::contract::virtual_* v = 0) /* override */ { // For virtuals.
57 boost::contract::old_ptr<unsigned> old_size =
58 BOOST_CONTRACT_OLDOF(v, size()); // Old values for virtuals.
59 boost::contract::check c = boost::contract::public_function< // For overrides.
60 override_push_back>(v, &vector::push_back, this, value)
61 .precondition([&] { // Checked in OR with base preconditions.
62 BOOST_CONTRACT_ASSERT(size() < max_size());
63 })
64 .postcondition([&] { // Checked in AND with base postconditions.
65 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
66 })
67 ;
68
69 vect_.push_back(value);
70 }
BOOST_CONTRACT_OVERRIDE(push_back)71 BOOST_CONTRACT_OVERRIDE(push_back) // Define `override_push_back` above.
72
73 // Could program contracts for those as well.
74 unsigned size() const { return vect_.size(); }
max_size() const75 unsigned max_size() const { return vect_.max_size(); }
capacity() const76 unsigned capacity() const { return vect_.capacity(); }
77
78 private:
79 std::vector<T> vect_;
80 };
81 //]
82
main()83 int main() {
84 vector<int> vect;
85 vect.push_back(123);
86 assert(vect.size() == 1);
87 return 0;
88 }
89
90