1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192 |
- // Copyright (C) 2008-2018 Lorenzo Caminiti
- // Distributed under the Boost Software License, Version 1.0 (see accompanying
- // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
- // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
- #include "no_lambdas.hpp"
- #include <boost/bind.hpp>
- #include <cassert>
- //[no_lambdas_cpp
- iarray::iarray(unsigned max, unsigned count) :
- boost::contract::constructor_precondition<iarray>(boost::bind(
- &iarray::constructor_precondition, max, count)),
- values_(new int[max]), // Member initializations can be here.
- capacity_(max)
- {
- boost::contract::old_ptr<int> old_instances;
- boost::contract::check c = boost::contract::constructor(this)
- .old(boost::bind(&iarray::constructor_old, boost::ref(old_instances)))
- .postcondition(boost::bind(
- &iarray::constructor_postcondition,
- this,
- boost::cref(max),
- boost::cref(count),
- boost::cref(old_instances)
- ))
- ;
- for(unsigned i = 0; i < count; ++i) values_[i] = int();
- size_ = count;
- ++instances_;
- }
- iarray::~iarray() {
- boost::contract::old_ptr<int> old_instances;
- boost::contract::check c = boost::contract::destructor(this)
- .old(boost::bind(&iarray::destructor_old, this,
- boost::ref(old_instances)))
- .postcondition(boost::bind(&iarray::destructor_postcondition,
- boost::cref(old_instances)))
- ;
-
- delete[] values_;
- --instances_;
- }
- void iarray::push_back(int value, boost::contract::virtual_* v) {
- boost::contract::old_ptr<unsigned> old_size;
- boost::contract::check c = boost::contract::public_function(v, this)
- .precondition(boost::bind(&iarray::push_back_precondition, this))
- .old(boost::bind(&iarray::push_back_old, this, boost::cref(v),
- boost::ref(old_size)))
- .postcondition(boost::bind(&iarray::push_back_postcondition, this,
- boost::cref(old_size)))
- ;
- values_[size_++] = value;
- }
- unsigned iarray::capacity() const {
- // Check invariants.
- boost::contract::check c = boost::contract::public_function(this);
- return capacity_;
- }
- unsigned iarray::size() const {
- // Check invariants.
- boost::contract::check c = boost::contract::public_function(this);
- return size_;
- }
- int iarray::instances() {
- // Check static invariants.
- boost::contract::check c = boost::contract::public_function<iarray>();
- return instances_;
- }
- int iarray::instances_ = 0;
- //]
- int main() {
- iarray a(3, 2);
- assert(a.capacity() == 3);
- assert(a.size() == 2);
-
- a.push_back(-123);
- assert(a.size() == 3);
- return 0;
- }
|