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 //[cline90_calendar 8 #include <boost/contract.hpp> 9 #include <cassert> 10 11 class calendar { 12 friend class boost::contract::access; 13 invariant() const14 void invariant() const { 15 BOOST_CONTRACT_ASSERT(month() >= 1); 16 BOOST_CONTRACT_ASSERT(month() <= 12); 17 BOOST_CONTRACT_ASSERT(date() >= 1); 18 BOOST_CONTRACT_ASSERT(date() <= days_in(month())); 19 } 20 21 public: calendar()22 calendar() : month_(1), date_(31) { 23 boost::contract::check c = boost::contract::constructor(this) 24 .postcondition([&] { 25 BOOST_CONTRACT_ASSERT(month() == 1); 26 BOOST_CONTRACT_ASSERT(date() == 31); 27 }) 28 ; 29 } 30 ~calendar()31 virtual ~calendar() { 32 // Check invariants. 33 boost::contract::check c = boost::contract::destructor(this); 34 } 35 month() const36 int month() const { 37 // Check invariants. 38 boost::contract::check c = boost::contract::public_function(this); 39 return month_; 40 } 41 date() const42 int date() const { 43 // Check invariants. 44 boost::contract::check c = boost::contract::public_function(this); 45 return date_; 46 } 47 reset(int new_month)48 void reset(int new_month) { 49 boost::contract::check c = boost::contract::public_function(this) 50 .precondition([&] { 51 BOOST_CONTRACT_ASSERT(new_month >= 1); 52 BOOST_CONTRACT_ASSERT(new_month <= 12); 53 }) 54 .postcondition([&] { 55 BOOST_CONTRACT_ASSERT(month() == new_month); 56 }) 57 ; 58 59 month_ = new_month; 60 } 61 62 private: days_in(int month)63 static int days_in(int month) { 64 int result; 65 boost::contract::check c = boost::contract::function() 66 .precondition([&] { 67 BOOST_CONTRACT_ASSERT(month >= 1); 68 BOOST_CONTRACT_ASSERT(month <= 12); 69 }) 70 .postcondition([&] { 71 BOOST_CONTRACT_ASSERT(result >= 1); 72 BOOST_CONTRACT_ASSERT(result <= 31); 73 }) 74 ; 75 76 return result = 31; // For simplicity, assume all months have 31 days. 77 } 78 79 int month_, date_; 80 }; 81 main()82int main() { 83 calendar cal; 84 assert(cal.date() == 31); 85 assert(cal.month() == 1); 86 87 cal.reset(8); // Set month 88 assert(cal.month() == 8); 89 90 return 0; 91 } 92 //] 93 94