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
12iarray::iarray(unsigned max, unsigned count) :
13 boost::contract::constructor_precondition<iarray>(boost::bind(
14 f: &iarray::constructor_precondition, a1: max, a2: 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(obj: this)
20 .old(f: boost::bind(f: &iarray::constructor_old, a1: boost::ref(t&: old_instances)))
21 .postcondition(f: boost::bind(
22 f: &iarray::constructor_postcondition,
23 a1: this,
24 a2: boost::cref(t: max),
25 a3: boost::cref(t: count),
26 a4: boost::cref(t: old_instances)
27 ))
28 ;
29
30 for(unsigned i = 0; i < count; ++i) values_[i] = int();
31 size_ = count;
32 ++instances_;
33}
34
35iarray::~iarray() {
36 boost::contract::old_ptr<int> old_instances;
37 boost::contract::check c = boost::contract::destructor(obj: this)
38 .old(f: boost::bind(f: &iarray::destructor_old, a1: this,
39 a2: boost::ref(t&: old_instances)))
40 .postcondition(f: boost::bind(f: &iarray::destructor_postcondition,
41 a1: boost::cref(t: old_instances)))
42 ;
43
44 delete[] values_;
45 --instances_;
46}
47
48void 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, obj: this)
51 .precondition(f: boost::bind(f: &iarray::push_back_precondition, a1: this))
52 .old(f: boost::bind(f: &iarray::push_back_old, a1: this, a2: boost::cref(t: v),
53 a3: boost::ref(t&: old_size)))
54 .postcondition(f: boost::bind(f: &iarray::push_back_postcondition, a1: this,
55 a2: boost::cref(t: old_size)))
56 ;
57
58 values_[size_++] = value;
59}
60
61unsigned iarray::capacity() const {
62 // Check invariants.
63 boost::contract::check c = boost::contract::public_function(obj: this);
64 return capacity_;
65}
66
67unsigned iarray::size() const {
68 // Check invariants.
69 boost::contract::check c = boost::contract::public_function(obj: this);
70 return size_;
71}
72
73int iarray::instances() {
74 // Check static invariants.
75 boost::contract::check c = boost::contract::public_function<iarray>();
76 return instances_;
77}
78
79int iarray::instances_ = 0;
80//]
81
82int main() {
83 iarray a(3, 2);
84 assert(a.capacity() == 3);
85 assert(a.size() == 2);
86
87 a.push_back(value: -123);
88 assert(a.size() == 3);
89
90 return 0;
91}
92
93

source code of boost/libs/contract/example/features/no_lambdas.cpp