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 <boost/contract.hpp> 8 #include <cassert> 9 #include <vector> 10 11 //[old_no_macro 12 template<typename T> 13 class vector { 14 public: push_back(T const & value,boost::contract::virtual_ * v=0)15 virtual void push_back(T const& value, boost::contract::virtual_* v = 0) { 16 // Program old value instead of using `OLD(size())` macro. 17 boost::contract::old_ptr<unsigned> old_size = 18 boost::contract::make_old(v, boost::contract::copy_old(v) ? 19 size() : boost::contract::null_old()) 20 ; 21 22 boost::contract::check c = boost::contract::public_function(v, this) 23 .postcondition([&] { 24 BOOST_CONTRACT_ASSERT(size() == *old_size + 1); 25 }) 26 ; 27 28 vect_.push_back(value); 29 } 30 31 /* ... */ 32 //] 33 size() const34 unsigned size() const { return vect_.size(); } 35 36 private: 37 std::vector<T> vect_; 38 }; 39 main()40int main() { 41 vector<int> vect; 42 vect.push_back(123); 43 assert(vect.size() == 1); 44 return 0; 45 } 46 47