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 "no_lambdas.hpp"
8 #include <boost/bind.hpp>
9 #include <cassert>
10
11 //[no_lambdas_cpp
iarray(unsigned max,unsigned count)12 iarray::iarray(unsigned max, unsigned count) :
13 boost::contract::constructor_precondition<iarray>(boost::bind(
14 &iarray::constructor_precondition, max, count)),
15 values_(new int[max]), // Member initializations can be here.
16 capacity_(max)
17 {
18 boost::contract::old_ptr<int> old_instances;
19 boost::contract::check c = boost::contract::constructor(this)
20 .old(boost::bind(&iarray::constructor_old, boost::ref(old_instances)))
21 .postcondition(boost::bind(
22 &iarray::constructor_postcondition,
23 this,
24 boost::cref(max),
25 boost::cref(count),
26 boost::cref(old_instances)
27 ))
28 ;
29
30 for(unsigned i = 0; i < count; ++i) values_[i] = int();
31 size_ = count;
32 ++instances_;
33 }
34
~iarray()35 iarray::~iarray() {
36 boost::contract::old_ptr<int> old_instances;
37 boost::contract::check c = boost::contract::destructor(this)
38 .old(boost::bind(&iarray::destructor_old, this,
39 boost::ref(old_instances)))
40 .postcondition(boost::bind(&iarray::destructor_postcondition,
41 boost::cref(old_instances)))
42 ;
43
44 delete[] values_;
45 --instances_;
46 }
47
push_back(int value,boost::contract::virtual_ * v)48 void iarray::push_back(int value, boost::contract::virtual_* v) {
49 boost::contract::old_ptr<unsigned> old_size;
50 boost::contract::check c = boost::contract::public_function(v, this)
51 .precondition(boost::bind(&iarray::push_back_precondition, this))
52 .old(boost::bind(&iarray::push_back_old, this, boost::cref(v),
53 boost::ref(old_size)))
54 .postcondition(boost::bind(&iarray::push_back_postcondition, this,
55 boost::cref(old_size)))
56 ;
57
58 values_[size_++] = value;
59 }
60
capacity() const61 unsigned iarray::capacity() const {
62 // Check invariants.
63 boost::contract::check c = boost::contract::public_function(this);
64 return capacity_;
65 }
66
size() const67 unsigned iarray::size() const {
68 // Check invariants.
69 boost::contract::check c = boost::contract::public_function(this);
70 return size_;
71 }
72
instances()73 int iarray::instances() {
74 // Check static invariants.
75 boost::contract::check c = boost::contract::public_function<iarray>();
76 return instances_;
77 }
78
79 int iarray::instances_ = 0;
80 //]
81
main()82 int main() {
83 iarray a(3, 2);
84 assert(a.capacity() == 3);
85 assert(a.size() == 2);
86
87 a.push_back(-123);
88 assert(a.size() == 3);
89
90 return 0;
91 }
92
93