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 <boost/local_function.hpp>
9 #include <boost/bind.hpp>
10 #include <cassert>
11
12 class iarray :
13 private boost::contract::constructor_precondition<iarray> {
14 public:
static_invariant()15 static void static_invariant() {
16 BOOST_CONTRACT_ASSERT(instances() >= 0);
17 }
18
invariant() const19 void invariant() const {
20 BOOST_CONTRACT_ASSERT(size() <= capacity());
21 }
22
constructor_pre(unsigned const max,unsigned const count)23 static void constructor_pre(unsigned const max, unsigned const count) {
24 BOOST_CONTRACT_ASSERT(count <= max);
25 }
iarray(unsigned max,unsigned count=0)26 explicit iarray(unsigned max, unsigned count = 0) :
27 boost::contract::constructor_precondition<iarray>(boost::bind(
28 &iarray::constructor_pre, max, count)),
29 values_(new int[max]),
30 capacity_(max)
31 {
32 boost::contract::old_ptr<int> old_instances;
33 void BOOST_LOCAL_FUNCTION(bind& old_instances) {
34 old_instances = BOOST_CONTRACT_OLDOF(iarray::instances());
35 } BOOST_LOCAL_FUNCTION_NAME(old)
36 void BOOST_LOCAL_FUNCTION(const bind this_, const bind& count,
37 const bind& old_instances) {
38 BOOST_CONTRACT_ASSERT(this_->size() == count);
39 BOOST_CONTRACT_ASSERT(this_->instances() == *old_instances + 1);
40 } BOOST_LOCAL_FUNCTION_NAME(post)
41 boost::contract::check c = boost::contract::constructor(this)
42 .old(old).postcondition(post);
43
44 for(unsigned i = 0; i < count; ++i) values_[i] = int();
45 size_ = count;
46 ++instances_;
47 }
48
~iarray()49 virtual ~iarray() {
50 boost::contract::old_ptr<int> old_instances;
51 void BOOST_LOCAL_FUNCTION(const bind this_, bind& old_instances) {
52 old_instances = BOOST_CONTRACT_OLDOF(this_->instances());
53 } BOOST_LOCAL_FUNCTION_NAME(old)
54 void BOOST_LOCAL_FUNCTION(const bind& old_instances) {
55 BOOST_CONTRACT_ASSERT(iarray::instances() == *old_instances - 1);
56 } BOOST_LOCAL_FUNCTION_NAME(post)
57 boost::contract::check c = boost::contract::destructor(this)
58 .old(old).postcondition(post);
59
60 delete[] values_;
61 --instances_;
62 }
63
push_back(int value,boost::contract::virtual_ * v=0)64 virtual void push_back(int value, boost::contract::virtual_* v = 0) {
65 boost::contract::old_ptr<unsigned> old_size;
66 void BOOST_LOCAL_FUNCTION(const bind this_) {
67 BOOST_CONTRACT_ASSERT(this_->size() < this_->capacity());
68 } BOOST_LOCAL_FUNCTION_NAME(pre)
69 void BOOST_LOCAL_FUNCTION(const bind v, const bind this_,
70 bind& old_size) {
71 old_size = BOOST_CONTRACT_OLDOF(v, this_->size());
72 } BOOST_LOCAL_FUNCTION_NAME(old)
73 void BOOST_LOCAL_FUNCTION(const bind this_, const bind& old_size) {
74 BOOST_CONTRACT_ASSERT(this_->size() == *old_size + 1);
75 } BOOST_LOCAL_FUNCTION_NAME(post)
76 boost::contract::check c = boost::contract::public_function(v, this)
77 .precondition(pre).old(old).postcondition(post);
78
79 values_[size_++] = value;
80 }
81
capacity() const82 unsigned capacity() const {
83 // Check invariants.
84 boost::contract::check c = boost::contract::public_function(this);
85 return capacity_;
86 }
87
size() const88 unsigned size() const {
89 // Check invariants.
90 boost::contract::check c = boost::contract::public_function(this);
91 return size_;
92 }
93
instances()94 static int instances() {
95 // Check static invariants.
96 boost::contract::check c = boost::contract::public_function<iarray>();
97 return instances_;
98 }
99
100 private:
101 int* values_;
102 unsigned capacity_;
103 unsigned size_;
104 static int instances_;
105 };
106
107 int iarray::instances_ = 0;
108
main()109 int main() {
110 iarray a(3, 2);
111 assert(a.capacity() == 3);
112 assert(a.size() == 2);
113
114 a.push_back('x');
115 assert(a.size() == 3);
116
117 return 0;
118 }
119
120