ceph/src/boost/libs/contract/example/mitchell02/courier.cpp

   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_courier
   8 #include <boost/contract.hpp>
   9 #include <string>
  10 #include <cassert>
  11
  12 struct package {
  13     double weight_kg;
  14     std::string location;
  15     double accepted_hour;
  16     double delivered_hour;
  17
  18     explicit package(
  19         double _weight_kg,
  20         std::string const& _location = "",
  21         double _accepted_hour = 0.0,
  22         double _delivered_hour = 0.0
  23     ) :
  24         weight_kg(_weight_kg),
  25         location(_location),
  26         accepted_hour(_accepted_hour),
  27         delivered_hour(_delivered_hour)
  28     {}
  29 };
  30
  31 // Courier for package delivery.
  32 class courier
  33     #define BASES private boost::contract::constructor_precondition<courier>
  34     : BASES
  35 {
  36     friend class boost::contract::access;
  37
  38     typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
  39     #undef BASES
  40
  41     static void static_invariant() {
  42         // Positive min. insurance.
  43         BOOST_CONTRACT_ASSERT(min_insurance_usd >= 0.0);
  44     }
  45
  46     void invariant() const {
  47         // Above min. insurance.
  48         BOOST_CONTRACT_ASSERT(insurance_cover_usd() >= min_insurance_usd);
  49     }
  50
  51 public:
  52     static double min_insurance_usd;
  53
  54     /* Creation */
  55
  56     // Create courier with specified insurance value.
  57     explicit courier(double _insurance_cover_usd = min_insurance_usd) :
  58         boost::contract::constructor_precondition<courier>([&] {
  59             // Positive insurance.
  60             BOOST_CONTRACT_ASSERT(_insurance_cover_usd >= 0.0);
  61         }),
  62         insurance_cover_usd_(_insurance_cover_usd)
  63     {
  64         // Check invariants.
  65         boost::contract::check c = boost::contract::constructor(this);
  66     }
  67
  68     // Destroy courier.
  69     virtual ~courier() {
  70         // Check invariants.
  71         boost::contract::check c = boost::contract::destructor(this);
  72     }
  73
  74     /* Queries */
  75
  76     // Return insurance cover.
  77     double insurance_cover_usd() const {
  78         // Check invariants.
  79         boost::contract::check c = boost::contract::public_function(this);
  80         return insurance_cover_usd_;
  81     }
  82
  83     /* Commands */
  84
  85     // Deliver package to destination.
  86     virtual void deliver(
  87         package& package_delivery,
  88         std::string const& destination,
  89         boost::contract::virtual_* v = 0
  90     ) {
  91         boost::contract::check c = boost::contract::public_function(v, this)
  92             .precondition([&] {
  93                 // Within max weight of this delivery.
  94                 BOOST_CONTRACT_ASSERT(package_delivery.weight_kg < 5.0);
  95             })
  96             .postcondition([&] {
  97                 // Within max delivery type.
  98                 BOOST_CONTRACT_ASSERT(double(package_delivery.delivered_hour -
  99                         package_delivery.accepted_hour) <= 3.0);
 100                 // Delivered at destination.
 101                 BOOST_CONTRACT_ASSERT(package_delivery.location == destination);
 102             })
 103         ;
 104
 105         package_delivery.location = destination;
 106         // Delivery takes 2.5 hours.
 107         package_delivery.delivered_hour = package_delivery.accepted_hour + 2.5;
 108     }
 109
 110 private:
 111     double insurance_cover_usd_;
 112 };
 113
 114 double courier::min_insurance_usd = 10.0e+6;
 115
 116 // Different courier for package delivery.
 117 class different_courier
 118     #define BASES private boost::contract::constructor_precondition< \
 119             different_courier>, public courier
 120     : BASES
 121 {
 122     friend class boost::contract::access;
 123
 124     typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting.
 125     #undef BASES
 126
 127     static void static_invariant() {
 128         BOOST_CONTRACT_ASSERT( // Better insurance amount.
 129                 different_insurance_usd >= courier::min_insurance_usd);
 130     }
 131
 132     void invariant() const {
 133         // Above different insurance value.
 134         BOOST_CONTRACT_ASSERT(insurance_cover_usd() >= different_insurance_usd);
 135     }
 136
 137     BOOST_CONTRACT_OVERRIDE(deliver)
 138
 139 public:
 140     static double different_insurance_usd;
 141
 142     /* Creation */
 143
 144     // Create courier with specified insurance value.
 145     explicit different_courier(
 146             double insurance_cover_usd = different_insurance_usd) :
 147         boost::contract::constructor_precondition<different_courier>([&] {
 148             // Positive insurance value.
 149             BOOST_CONTRACT_ASSERT(insurance_cover_usd > 0.0);
 150         }),
 151         courier(insurance_cover_usd)
 152     {
 153         // Check invariants.
 154         boost::contract::check c = boost::contract::constructor(this);
 155     }
 156
 157     // Destroy courier.
 158     virtual ~different_courier() {
 159         // Check invariants.
 160         boost::contract::check c = boost::contract::destructor(this);
 161     }
 162
 163     /* Commands */
 164
 165     virtual void deliver(
 166         package& package_delivery,
 167         std::string const& destination,
 168         boost::contract::virtual_* v = 0
 169     ) /* override */ {
 170         boost::contract::check c = boost::contract::public_function<
 171             override_deliver
 172         >(v, &different_courier::deliver, this, package_delivery, destination)
 173             .precondition([&] {
 174                 // Package can weight more (weaker precondition).
 175                 BOOST_CONTRACT_ASSERT(package_delivery.weight_kg <= 8.0);
 176             })
 177             .postcondition([&] {
 178                 // Faster delivery (stronger postcondition).
 179                 BOOST_CONTRACT_ASSERT(double(package_delivery.delivered_hour -
 180                         package_delivery.accepted_hour) <= 2.0);
 181                 // Inherited "delivery at destination" postcondition.
 182             })
 183         ;
 184
 185         package_delivery.location = destination;
 186         // Delivery takes 0.5 hours.
 187         package_delivery.delivered_hour = package_delivery.accepted_hour + 0.5;
 188     }
 189 };
 190
 191 double different_courier::different_insurance_usd = 20.0e+6;
 192
 193 int main() {
 194     package cups(3.6, "store");
 195     courier c;
 196     c.deliver(cups, "home");
 197     assert(cups.location == "home");
 198
 199     package desk(7.2, "store");
 200     different_courier dc;
 201     dc.deliver(desk, "office");
 202     assert(desk.location == "office");
 203
 204     return 0;
 205 }
 206 //]
 207