1 2 #ifndef NO_LAMBDAS_HPP_ 3 #define NO_LAMBDAS_HPP_ 4 5 // Copyright (C) 2008-2018 Lorenzo Caminiti 6 // Distributed under the Boost Software License, Version 1.0 (see accompanying 7 // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt). 8 // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html 9 10 #include <boost/contract.hpp> 11 12 //[no_lambdas_hpp 13 class iarray : 14 private boost::contract::constructor_precondition<iarray> { 15 public: static_invariant()16 static void static_invariant() { 17 BOOST_CONTRACT_ASSERT(instances() >= 0); 18 } 19 invariant() const20 void invariant() const { 21 BOOST_CONTRACT_ASSERT(size() <= capacity()); 22 } 23 24 explicit iarray(unsigned max, unsigned count = 0); constructor_precondition(unsigned const max,unsigned const count)25 static void constructor_precondition(unsigned const max, 26 unsigned const count) { 27 BOOST_CONTRACT_ASSERT(count <= max); 28 } constructor_old(boost::contract::old_ptr<int> & old_instances)29 static void constructor_old(boost::contract::old_ptr<int>& 30 old_instances) { 31 old_instances = BOOST_CONTRACT_OLDOF(instances()); 32 } constructor_postcondition(unsigned const max,unsigned const count,boost::contract::old_ptr<int> const old_instances) const33 void constructor_postcondition(unsigned const max, unsigned const count, 34 boost::contract::old_ptr<int> const old_instances) const { 35 BOOST_CONTRACT_ASSERT(capacity() == max); 36 BOOST_CONTRACT_ASSERT(size() == count); 37 BOOST_CONTRACT_ASSERT(instances() == *old_instances + 1); 38 } 39 40 virtual ~iarray(); destructor_old(boost::contract::old_ptr<int> & old_instances) const41 void destructor_old(boost::contract::old_ptr<int>& old_instances) 42 const { 43 old_instances = BOOST_CONTRACT_OLDOF(instances()); 44 } destructor_postcondition(boost::contract::old_ptr<int> const old_instances)45 static void destructor_postcondition(boost::contract::old_ptr<int> const 46 old_instances) { 47 BOOST_CONTRACT_ASSERT(instances() == *old_instances - 1); 48 } 49 50 virtual void push_back(int value, boost::contract::virtual_* v = 0); push_back_precondition() const51 void push_back_precondition() const { 52 BOOST_CONTRACT_ASSERT(size() < capacity()); 53 } push_back_old(boost::contract::virtual_ * v,boost::contract::old_ptr<unsigned> & old_size) const54 void push_back_old(boost::contract::virtual_* v, 55 boost::contract::old_ptr<unsigned>& old_size) const { 56 old_size = BOOST_CONTRACT_OLDOF(v, size()); 57 } push_back_postcondition(boost::contract::old_ptr<unsigned> const old_size) const58 void push_back_postcondition( 59 boost::contract::old_ptr<unsigned> const old_size) const { 60 BOOST_CONTRACT_ASSERT(size() == *old_size + 1); 61 } 62 63 unsigned capacity() const; 64 unsigned size() const; 65 66 static int instances(); 67 68 private: 69 int* values_; 70 unsigned capacity_; 71 unsigned size_; 72 static int instances_; 73 }; 74 //] 75 76 #endif // #include guard 77 78