calendar.cpp 2.5 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293
  1. // Copyright (C) 2008-2018 Lorenzo Caminiti
  2. // Distributed under the Boost Software License, Version 1.0 (see accompanying
  3. // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
  4. // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
  5. //[cline90_calendar
  6. #include <boost/contract.hpp>
  7. #include <cassert>
  8. class calendar {
  9. friend class boost::contract::access;
  10. void invariant() const {
  11. BOOST_CONTRACT_ASSERT(month() >= 1);
  12. BOOST_CONTRACT_ASSERT(month() <= 12);
  13. BOOST_CONTRACT_ASSERT(date() >= 1);
  14. BOOST_CONTRACT_ASSERT(date() <= days_in(month()));
  15. }
  16. public:
  17. calendar() : month_(1), date_(31) {
  18. boost::contract::check c = boost::contract::constructor(this)
  19. .postcondition([&] {
  20. BOOST_CONTRACT_ASSERT(month() == 1);
  21. BOOST_CONTRACT_ASSERT(date() == 31);
  22. })
  23. ;
  24. }
  25. virtual ~calendar() {
  26. // Check invariants.
  27. boost::contract::check c = boost::contract::destructor(this);
  28. }
  29. int month() const {
  30. // Check invariants.
  31. boost::contract::check c = boost::contract::public_function(this);
  32. return month_;
  33. }
  34. int date() const {
  35. // Check invariants.
  36. boost::contract::check c = boost::contract::public_function(this);
  37. return date_;
  38. }
  39. void reset(int new_month) {
  40. boost::contract::check c = boost::contract::public_function(this)
  41. .precondition([&] {
  42. BOOST_CONTRACT_ASSERT(new_month >= 1);
  43. BOOST_CONTRACT_ASSERT(new_month <= 12);
  44. })
  45. .postcondition([&] {
  46. BOOST_CONTRACT_ASSERT(month() == new_month);
  47. })
  48. ;
  49. month_ = new_month;
  50. }
  51. private:
  52. static int days_in(int month) {
  53. int result;
  54. boost::contract::check c = boost::contract::function()
  55. .precondition([&] {
  56. BOOST_CONTRACT_ASSERT(month >= 1);
  57. BOOST_CONTRACT_ASSERT(month <= 12);
  58. })
  59. .postcondition([&] {
  60. BOOST_CONTRACT_ASSERT(result >= 1);
  61. BOOST_CONTRACT_ASSERT(result <= 31);
  62. })
  63. ;
  64. return result = 31; // For simplicity, assume all months have 31 days.
  65. }
  66. int month_, date_;
  67. };
  68. int main() {
  69. calendar cal;
  70. assert(cal.date() == 31);
  71. assert(cal.month() == 1);
  72. cal.reset(8); // Set month
  73. assert(cal.month() == 8);
  74. return 0;
  75. }
  76. //]