78 lines
2.5 KiB
C++
78 lines
2.5 KiB
C++
|
|
#ifndef NO_LAMBDAS_HPP_
|
|
#define NO_LAMBDAS_HPP_
|
|
|
|
// 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 <boost/contract.hpp>
|
|
|
|
//[no_lambdas_hpp
|
|
class iarray :
|
|
private boost::contract::constructor_precondition<iarray> {
|
|
public:
|
|
static void static_invariant() {
|
|
BOOST_CONTRACT_ASSERT(instances() >= 0);
|
|
}
|
|
|
|
void invariant() const {
|
|
BOOST_CONTRACT_ASSERT(size() <= capacity());
|
|
}
|
|
|
|
explicit iarray(unsigned max, unsigned count = 0);
|
|
static void constructor_precondition(unsigned const max,
|
|
unsigned const count) {
|
|
BOOST_CONTRACT_ASSERT(count <= max);
|
|
}
|
|
static void constructor_old(boost::contract::old_ptr<int>&
|
|
old_instances) {
|
|
old_instances = BOOST_CONTRACT_OLDOF(instances());
|
|
}
|
|
void constructor_postcondition(unsigned const max, unsigned const count,
|
|
boost::contract::old_ptr<int> const old_instances) const {
|
|
BOOST_CONTRACT_ASSERT(capacity() == max);
|
|
BOOST_CONTRACT_ASSERT(size() == count);
|
|
BOOST_CONTRACT_ASSERT(instances() == *old_instances + 1);
|
|
}
|
|
|
|
virtual ~iarray();
|
|
void destructor_old(boost::contract::old_ptr<int>& old_instances)
|
|
const {
|
|
old_instances = BOOST_CONTRACT_OLDOF(instances());
|
|
}
|
|
static void destructor_postcondition(boost::contract::old_ptr<int> const
|
|
old_instances) {
|
|
BOOST_CONTRACT_ASSERT(instances() == *old_instances - 1);
|
|
}
|
|
|
|
virtual void push_back(int value, boost::contract::virtual_* v = 0);
|
|
void push_back_precondition() const {
|
|
BOOST_CONTRACT_ASSERT(size() < capacity());
|
|
}
|
|
void push_back_old(boost::contract::virtual_* v,
|
|
boost::contract::old_ptr<unsigned>& old_size) const {
|
|
old_size = BOOST_CONTRACT_OLDOF(v, size());
|
|
}
|
|
void push_back_postcondition(
|
|
boost::contract::old_ptr<unsigned> const old_size) const {
|
|
BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
|
|
}
|
|
|
|
unsigned capacity() const;
|
|
unsigned size() const;
|
|
|
|
static int instances();
|
|
|
|
private:
|
|
int* values_;
|
|
unsigned capacity_;
|
|
unsigned size_;
|
|
static int instances_;
|
|
};
|
|
//]
|
|
|
|
#endif // #include guard
|
|
|