123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293 |
- // Copyright (C) 2008-2018 Lorenzo Caminiti
- // Distributed under the Boost Software License, Version 1.0 (see accompanying
- // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
- // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
- //[cline90_calendar
- #include <boost/contract.hpp>
- #include <cassert>
- class calendar {
- friend class boost::contract::access;
- void invariant() const {
- BOOST_CONTRACT_ASSERT(month() >= 1);
- BOOST_CONTRACT_ASSERT(month() <= 12);
- BOOST_CONTRACT_ASSERT(date() >= 1);
- BOOST_CONTRACT_ASSERT(date() <= days_in(month()));
- }
- public:
- calendar() : month_(1), date_(31) {
- boost::contract::check c = boost::contract::constructor(this)
- .postcondition([&] {
- BOOST_CONTRACT_ASSERT(month() == 1);
- BOOST_CONTRACT_ASSERT(date() == 31);
- })
- ;
- }
- virtual ~calendar() {
- // Check invariants.
- boost::contract::check c = boost::contract::destructor(this);
- }
- int month() const {
- // Check invariants.
- boost::contract::check c = boost::contract::public_function(this);
- return month_;
- }
- int date() const {
- // Check invariants.
- boost::contract::check c = boost::contract::public_function(this);
- return date_;
- }
- void reset(int new_month) {
- boost::contract::check c = boost::contract::public_function(this)
- .precondition([&] {
- BOOST_CONTRACT_ASSERT(new_month >= 1);
- BOOST_CONTRACT_ASSERT(new_month <= 12);
- })
- .postcondition([&] {
- BOOST_CONTRACT_ASSERT(month() == new_month);
- })
- ;
- month_ = new_month;
- }
- private:
- static int days_in(int month) {
- int result;
- boost::contract::check c = boost::contract::function()
- .precondition([&] {
- BOOST_CONTRACT_ASSERT(month >= 1);
- BOOST_CONTRACT_ASSERT(month <= 12);
- })
- .postcondition([&] {
- BOOST_CONTRACT_ASSERT(result >= 1);
- BOOST_CONTRACT_ASSERT(result <= 31);
- })
- ;
- return result = 31; // For simplicity, assume all months have 31 days.
- }
- int month_, date_;
- };
- int main() {
- calendar cal;
- assert(cal.date() == 31);
- assert(cal.month() == 1);
- cal.reset(8); // Set month
- assert(cal.month() == 8);
- return 0;
- }
- //]
|