ceph/src/boost/libs/contract/example/cline90/vstack.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 //[cline90_vstack
   8 #include "vector.hpp"
   9 #include <boost/contract.hpp>
  10 #include <boost/optional.hpp>
  11 #include <cassert>
  12
  13 // NOTE: Incomplete contract assertions, addressing only `empty` and `full`.
  14 template<typename T>
  15 class abstract_stack {
  16 public:
  17     abstract_stack() {
  18         boost::contract::check c = boost::contract::constructor(this)
  19             .postcondition([&] {
  20                 // AXIOM as empty() cannot actually be checked here to avoid
  21                 // calling pure virtual function length() during construction).
  22                 BOOST_CONTRACT_ASSERT_AXIOM(empty());
  23             })
  24         ;
  25     }
  26
  27     virtual ~abstract_stack() {
  28         boost::contract::check c = boost::contract::destructor(this);
  29     }
  30
  31     bool full() const {
  32         bool result;
  33         boost::contract::check c = boost::contract::public_function(this)
  34             .postcondition([&] {
  35                 BOOST_CONTRACT_ASSERT(result == (length() == capacity()));
  36             })
  37         ;
  38
  39         return result = (length() == capacity());
  40     }
  41
  42     bool empty() const {
  43         bool result;
  44         boost::contract::check c = boost::contract::public_function(this)
  45             .postcondition([&] {
  46                 BOOST_CONTRACT_ASSERT(result = (length() == 0));
  47             })
  48         ;
  49
  50         return result = (length() == 0);
  51     }
  52
  53     virtual int length(boost::contract::virtual_* v = 0) const = 0;
  54     virtual int capacity(boost::contract::virtual_* v = 0) const = 0;
  55
  56     virtual T const& item(boost::contract::virtual_* v = 0) const = 0;
  57
  58     virtual void push(T const& value, boost::contract::virtual_* v = 0) = 0;
  59     virtual T const& pop(boost::contract::virtual_* v = 0) = 0;
  60
  61     virtual void clear(boost::contract::virtual_* v = 0) = 0;
  62 };
  63
  64 template<typename T>
  65 int abstract_stack<T>::length(boost::contract::virtual_* v) const {
  66     int result;
  67     boost::contract::check c = boost::contract::public_function(v, result, this)
  68         .postcondition([&] (int const& result) {
  69             BOOST_CONTRACT_ASSERT(result >= 0);
  70         })
  71     ;
  72     assert(false);
  73     return result;
  74 }
  75
  76 template<typename T>
  77 int abstract_stack<T>::capacity(boost::contract::virtual_* v) const {
  78     int result;
  79     boost::contract::check c = boost::contract::public_function(v, result, this)
  80         .postcondition([&] (int const& result) {
  81             BOOST_CONTRACT_ASSERT(result >= 0);
  82         })
  83     ;
  84     assert(false);
  85     return result;
  86 }
  87
  88 template<typename T>
  89 T const& abstract_stack<T>::item(boost::contract::virtual_* v) const {
  90     boost::optional<T const&> result;
  91     boost::contract::check c = boost::contract::public_function(v, result, this)
  92         .precondition([&] {
  93             BOOST_CONTRACT_ASSERT(!empty());
  94         })
  95     ;
  96     assert(false);
  97     return *result;
  98 }
  99
 100 template<typename T>
 101 void abstract_stack<T>::push(T const& value, boost::contract::virtual_* v) {
 102     boost::contract::check c = boost::contract::public_function(v, this)
 103         .precondition([&] {
 104             BOOST_CONTRACT_ASSERT(!full());
 105         })
 106         .postcondition([&] {
 107             BOOST_CONTRACT_ASSERT(!empty());
 108         })
 109     ;
 110     assert(false);
 111 }
 112
 113 template<typename T>
 114 T const& abstract_stack<T>::pop(boost::contract::virtual_* v) {
 115     boost::optional<T const&> result;
 116     boost::contract::old_ptr<T> old_item = BOOST_CONTRACT_OLDOF(v, item());
 117     boost::contract::check c = boost::contract::public_function(v, result, this)
 118         .precondition([&] {
 119             BOOST_CONTRACT_ASSERT(!empty());
 120         })
 121         .postcondition([&] (boost::optional<T const&> const& result) {
 122             BOOST_CONTRACT_ASSERT(!full());
 123             BOOST_CONTRACT_ASSERT(*result == *old_item);
 124         })
 125     ;
 126     assert(false);
 127     return *result;
 128 }
 129
 130 template<typename T>
 131 void abstract_stack<T>::clear(boost::contract::virtual_* v) {
 132     boost::contract::check c = boost::contract::public_function(v, this)
 133         .postcondition([&] {
 134             BOOST_CONTRACT_ASSERT(empty());
 135         })
 136     ;
 137     assert(false);
 138 }
 139
 140 template<typename T>
 141 class vstack
 142     #define BASES private boost::contract::constructor_precondition< \
 143             vstack<T> >, public abstract_stack<T>
 144     : BASES
 145 {
 146     friend class boost::contract::access;
 147
 148     typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
 149     #undef BASES
 150
 151     void invariant() const {
 152         BOOST_CONTRACT_ASSERT(length() >= 0);
 153         BOOST_CONTRACT_ASSERT(length() < capacity());
 154     }
 155
 156     BOOST_CONTRACT_OVERRIDES(length, capacity, item, push, pop, clear)
 157
 158 public:
 159     explicit vstack(int count = 10) :
 160         boost::contract::constructor_precondition<vstack>([&] {
 161             BOOST_CONTRACT_ASSERT(count >= 0);
 162         }),
 163         vect_(count), // OK, executed after precondition so count >= 0.
 164         len_(0)
 165     {
 166         boost::contract::check c = boost::contract::constructor(this)
 167             .postcondition([&] {
 168                 BOOST_CONTRACT_ASSERT(length() == 0);
 169                 BOOST_CONTRACT_ASSERT(capacity() == count);
 170             })
 171         ;
 172     }
 173
 174     virtual ~vstack() {
 175         boost::contract::check c = boost::contract::destructor(this);
 176     }
 177
 178     // Inherited from abstract_stack.
 179
 180     virtual int length(boost::contract::virtual_* v = 0) const /* override */ {
 181         int result;
 182         boost::contract::check c = boost::contract::public_function<
 183                 override_length>(v, result, &vstack::length, this);
 184         return result = len_;
 185     }
 186
 187     virtual int capacity(boost::contract::virtual_* v = 0)
 188             const /* override */ {
 189         int result;
 190         boost::contract::check c = boost::contract::public_function<
 191                 override_capacity>(v, result, &vstack::capacity, this);
 192         return result = vect_.size();
 193     }
 194
 195     virtual T const& item(boost::contract::virtual_* v = 0)
 196             const /* override */ {
 197         boost::optional<T const&> result;
 198         boost::contract::check c = boost::contract::public_function<
 199                 override_item>(v, result, &vstack::item, this);
 200         return *(result = vect_[len_ - 1]);
 201     }
 202
 203     virtual void push(T const& value, boost::contract::virtual_* v = 0)
 204             /* override */ {
 205         boost::contract::check c = boost::contract::public_function<
 206                 override_push>(v, &vstack::push, this, value);
 207         vect_[len_++] = value;
 208     }
 209
 210     virtual T const& pop(boost::contract::virtual_* v = 0) /* override */ {
 211         boost::optional<T const&> result;
 212         boost::contract::check c = boost::contract::public_function<
 213                 override_pop>(v, result, &vstack::pop, this);
 214         return *(result = vect_[--len_]);
 215     }
 216
 217     virtual void clear(boost::contract::virtual_* v = 0) /* override */ {
 218         boost::contract::check c = boost::contract::public_function<
 219                 override_clear>(v, &vstack::clear, this);
 220         len_ = 0;
 221     }
 222
 223 private:
 224     vector<T> vect_;
 225     int len_;
 226 };
 227
 228 int main() {
 229     vstack<int> s(3);
 230     assert(s.capacity() == 3);
 231
 232     s.push(123);
 233     assert(s.length() == 1);
 234     assert(s.pop() == 123);
 235
 236     return 0;
 237 }
 238 //]
 239