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 <limits> 9 #include <cassert> 10 11 //[private_protected 12 class counter { 13 protected: // Protected functions use `function()` (like non-members). set(int n)14 void set(int n) { 15 boost::contract::check c = boost::contract::function() 16 .precondition([&] { 17 BOOST_CONTRACT_ASSERT(n <= 0); 18 }) 19 .postcondition([&] { 20 BOOST_CONTRACT_ASSERT(get() == n); 21 }) 22 ; 23 24 n_ = n; 25 } 26 27 private: // Private functions use `function()` (like non-members). dec()28 void dec() { 29 boost::contract::old_ptr<int> old_get = BOOST_CONTRACT_OLDOF(get()); 30 boost::contract::check c = boost::contract::function() 31 .precondition([&] { 32 BOOST_CONTRACT_ASSERT( 33 get() + 1 >= std::numeric_limits<int>::min()); 34 }) 35 .postcondition([&] { 36 BOOST_CONTRACT_ASSERT(get() == *old_get - 1); 37 }) 38 ; 39 40 set(get() - 1); 41 } 42 43 int n_; 44 45 /* ... */ 46 //] 47 48 public: get() const49 int get() const { 50 int result; 51 boost::contract::check c = boost::contract::public_function(this) 52 .postcondition([&] { 53 BOOST_CONTRACT_ASSERT(result <= 0); 54 BOOST_CONTRACT_ASSERT(result == n_); 55 }) 56 ; 57 58 return result = n_; 59 } 60 counter()61 counter() : n_(0) {} // Should contract constructor and destructor too. 62 invariant() const63 void invariant() const { 64 BOOST_CONTRACT_ASSERT(get() <= 0); 65 } 66 67 friend int main(); 68 }; 69 main()70int main() { 71 counter cnt; 72 assert(cnt.get() == 0); 73 cnt.dec(); 74 assert(cnt.get() == -1); 75 return 0; 76 } 77 78