1 2 #ifndef SEPARATE_BODY_HPP_ 3 #define SEPARATE_BODY_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 //[separate_body_hpp 13 class iarray : 14 private boost::contract::constructor_precondition<iarray> { 15 public: invariant() const16 void invariant() const { 17 BOOST_CONTRACT_ASSERT(size() <= capacity()); 18 } 19 iarray(unsigned max,unsigned count=0)20 explicit iarray(unsigned max, unsigned count = 0) : 21 boost::contract::constructor_precondition<iarray>([&] { 22 BOOST_CONTRACT_ASSERT(count <= max); 23 }), 24 // Still, member initializations must be here. 25 values_(new int[max]), 26 capacity_(max) 27 { 28 boost::contract::check c = boost::contract::constructor(this) __anon3fcb91e10202null29 .postcondition([&] { 30 BOOST_CONTRACT_ASSERT(capacity() == max); 31 BOOST_CONTRACT_ASSERT(size() == count); 32 }) 33 ; 34 constructor_body(max, count); // Separate constructor body impl. 35 } 36 ~iarray()37 virtual ~iarray() { 38 boost::contract::check c = boost::contract::destructor(this); // Inv. 39 destructor_body(); // Separate destructor body implementation. 40 } 41 push_back(int value,boost::contract::virtual_ * v=0)42 virtual void push_back(int value, boost::contract::virtual_* v = 0) { 43 boost::contract::old_ptr<unsigned> old_size = 44 BOOST_CONTRACT_OLDOF(v, size()); 45 boost::contract::check c = boost::contract::public_function(v, this) 46 .precondition([&] { 47 BOOST_CONTRACT_ASSERT(size() < capacity()); 48 }) 49 .postcondition([&] { 50 BOOST_CONTRACT_ASSERT(size() == *old_size + 1); 51 }) 52 ; 53 push_back_body(value); // Separate member function body implementation. 54 } 55 56 private: 57 // Contracts in class declaration (above), but body implementations are not. 58 void constructor_body(unsigned max, unsigned count); 59 void destructor_body(); 60 void push_back_body(int value); 61 62 /* ... */ 63 //] 64 65 public: capacity() const66 unsigned capacity() const { 67 // Check invariants. 68 boost::contract::check c = boost::contract::public_function(this); 69 return capacity_body(); 70 } 71 size() const72 unsigned size() const { 73 // Check invariants. 74 boost::contract::check c = boost::contract::public_function(this); 75 return size_body(); 76 } 77 78 private: 79 unsigned size_body() const; 80 unsigned capacity_body() const; 81 82 int* values_; 83 unsigned capacity_; 84 unsigned size_; 85 }; 86 87 #endif // #include guard 88 89