ceph/src/boost/libs/contract/example/mitchell02/counter/push_button.hpp

   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 //[mitchell02_push_button
   8 #ifndef PUSH_BUTTON_HPP_
   9 #define PUSH_BUTTON_HPP_
  10
  11 #include <boost/contract.hpp>
  12 #include <cassert>
  13
  14 class push_button {
  15 public:
  16     // No inv and no bases so contracts optional if no pre, post, and override.
  17
  18     /* Creation */
  19
  20     // Create an enabled button.
  21     push_button() : enabled_(true) {
  22         boost::contract::check c = boost::contract::constructor(this)
  23             .postcondition([&] {
  24                 BOOST_CONTRACT_ASSERT(enabled()); // Enabled.
  25             })
  26         ;
  27     }
  28
  29     // Destroy button.
  30     virtual ~push_button() {
  31         // Could have omitted contracts here (nothing to check).
  32         boost::contract::check c = boost::contract::destructor(this);
  33     }
  34
  35     /* Queries */
  36
  37     // If button is enabled.
  38     bool enabled() const {
  39         // Could have omitted contracts here (nothing to check).
  40         boost::contract::check c = boost::contract::public_function(this);
  41         return enabled_;
  42     }
  43
  44     /* Commands */
  45
  46     // Enable button.
  47     void enable() {
  48         boost::contract::check c = boost::contract::public_function(this)
  49             .postcondition([&] {
  50                 BOOST_CONTRACT_ASSERT(enabled()); // Enabled.
  51             })
  52         ;
  53
  54         enabled_ = true;
  55     }
  56
  57     // Disable button.
  58     void disable() {
  59         boost::contract::check c = boost::contract::public_function(this)
  60             .postcondition([&] {
  61                 BOOST_CONTRACT_ASSERT(!enabled()); // Disabled.
  62             })
  63         ;
  64
  65         enabled_ = false;
  66     }
  67
  68     // Invoke externally when button clicked.
  69     virtual void on_bn_clicked(boost::contract::virtual_* v = 0) = 0;
  70
  71 private:
  72     bool enabled_;
  73 };
  74
  75 void push_button::on_bn_clicked(boost::contract::virtual_* v) {
  76     boost::contract::check c = boost::contract::public_function(v, this)
  77         .precondition([&] {
  78             BOOST_CONTRACT_ASSERT(enabled()); // Enabled.
  79         })
  80     ;
  81     assert(false);
  82 }
  83
  84 #endif // #include guard
  85 //]
  86