libs/contract/example/features/public.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 #include <boost/contract.hpp>
   8 #include <vector>
   9 #include <algorithm>
  10 #include <cassert>
  11
  12 //[public_class_begin
  13 class unique_identifiers :
  14     private boost::contract::constructor_precondition<unique_identifiers>
  15 {
  16 public:
  17     void invariant() const {
  18         BOOST_CONTRACT_ASSERT(size() >= 0);
  19     }
  20 //]
  21
  22 //[public_constructor
  23 public:
  24     // Contract for a constructor.
  25     unique_identifiers(int from, int to) :
  26         boost::contract::constructor_precondition<unique_identifiers>([&] {
  27             BOOST_CONTRACT_ASSERT(from >= 0);
  28             BOOST_CONTRACT_ASSERT(to >= from);
  29         })
  30     {
  31         boost::contract::check c = boost::contract::constructor(this)
  32             .postcondition([&] {
  33                 BOOST_CONTRACT_ASSERT(size() == (to - from + 1));
  34             })
  35         ;
  36
  37         // Constructor body.
  38         for(int id = from; id <= to; ++id) vect_.push_back(id);
  39     }
  40 //]
  41
  42 //[public_destructor
  43 public:
  44     // Contract for a destructor.
  45     virtual ~unique_identifiers() {
  46         // Following contract checks class invariants.
  47         boost::contract::check c = boost::contract::destructor(this);
  48
  49         // Destructor body here... (do nothing in this example).
  50     }
  51 //]
  52
  53     int size() const {
  54         // Following contract checks invariants.
  55         boost::contract::check c = boost::contract::public_function(this);
  56         return vect_.size();
  57     }
  58
  59 //[public_function
  60 public:
  61     // Contract for a public function (but no static, virtual, or override).
  62     bool find(int id) const {
  63         bool result;
  64         boost::contract::check c = boost::contract::public_function(this)
  65             .precondition([&] {
  66                 BOOST_CONTRACT_ASSERT(id >= 0);
  67             })
  68             .postcondition([&] {
  69                 if(size() == 0) BOOST_CONTRACT_ASSERT(!result);
  70             })
  71         ;
  72
  73         // Function body.
  74         return result = std::find(vect_.begin(), vect_.end(), id) !=
  75                 vect_.end();
  76     }
  77 //]
  78
  79 //[public_virtual_function
  80 public:
  81     // Contract for a public virtual function (but no override).
  82     virtual int push_back(int id, boost::contract::virtual_* v = 0) { // Extra `v`.
  83         int result;
  84         boost::contract::old_ptr<bool> old_find =
  85                 BOOST_CONTRACT_OLDOF(v, find(id)); // Pass `v`.
  86         boost::contract::old_ptr<int> old_size =
  87                 BOOST_CONTRACT_OLDOF(v, size()); // Pass `v`.
  88         boost::contract::check c = boost::contract::public_function(
  89                 v, result, this) // Pass `v` and `result`.
  90             .precondition([&] {
  91                 BOOST_CONTRACT_ASSERT(id >= 0);
  92                 BOOST_CONTRACT_ASSERT(!find(id)); // ID cannot be already present.
  93             })
  94             .postcondition([&] (int const result) {
  95                 if(!*old_find) {
  96                     BOOST_CONTRACT_ASSERT(find(id));
  97                     BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
  98                 }
  99                 BOOST_CONTRACT_ASSERT(result == id);
 100             })
 101         ;
 102
 103         // Function body.
 104         vect_.push_back(id);
 105         return result = id;
 106     }
 107 //]
 108
 109 private:
 110     std::vector<int> vect_;
 111 //[public_class_end
 112     /* ... */
 113 };
 114 //]
 115
 116 //[public_derived_class_begin
 117 class identifiers
 118     #define BASES public unique_identifiers
 119     : BASES
 120 {
 121 public:
 122     typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Bases typedef.
 123     #undef BASES
 124
 125     void invariant() const { // Check in AND with bases.
 126         BOOST_CONTRACT_ASSERT(empty() == (size() == 0));
 127     }
 128 //]
 129
 130 //[public_function_override
 131 public:
 132     // Contract for a public function override.
 133     int push_back(int id, boost::contract::virtual_* v = 0) /* override */ {
 134         int result;
 135         boost::contract::old_ptr<bool> old_find =
 136                 BOOST_CONTRACT_OLDOF(v, find(id));
 137         boost::contract::old_ptr<int> old_size =
 138                 BOOST_CONTRACT_OLDOF(v, size());
 139         boost::contract::check c = boost::contract::public_function<
 140             override_push_back // Pass override type plus below function pointer...
 141         >(v, result, &identifiers::push_back, this, id) // ...and arguments.
 142             .precondition([&] { // Check in OR with bases.
 143                 BOOST_CONTRACT_ASSERT(id >= 0);
 144                 BOOST_CONTRACT_ASSERT(find(id)); // ID can be already present.
 145             })
 146             .postcondition([&] (int const result) { // Check in AND with bases.
 147                 if(*old_find) BOOST_CONTRACT_ASSERT(size() == *old_size);
 148             })
 149         ;
 150
 151         // Function body.
 152         if(!find(id)) unique_identifiers::push_back(id); // Else, do nothing.
 153         return result = id;
 154     }
 155     BOOST_CONTRACT_OVERRIDE(push_back) // Define `override_push_back`.
 156 //]
 157
 158     bool empty() const {
 159         // Following contract checks invariants.
 160         boost::contract::check c = boost::contract::public_function(this);
 161         return size() == 0;
 162     }
 163
 164     identifiers(int from, int to) : unique_identifiers(from, to) {
 165         // Following contract checks invariants.
 166         boost::contract::check c = boost::contract::constructor(this);
 167     }
 168
 169 //[public_derived_class_end
 170     /* ... */
 171 };
 172 //]
 173
 174 int main() {
 175     unique_identifiers uids(1, 4);
 176     assert(uids.find(2));
 177     assert(!uids.find(5));
 178     uids.push_back(5);
 179     assert(uids.find(5));
 180
 181     identifiers ids(10, 40);
 182     assert(!ids.find(50));
 183     ids.push_back(50);
 184     ids.push_back(50);
 185     assert(ids.find(50));
 186
 187     return 0;
 188 }
 189