ceph/src/boost/libs/contract/example/meyer97/stack4.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 //[meyer97_stack4
   8 // File: stack4.hpp
   9 #ifndef STACK4_HPP_
  10 #define STACK4_HPP_
  11
  12 #include <boost/contract.hpp>
  13
  14 // Dispenser with LIFO access policy and fixed max capacity.
  15 template<typename T>
  16 class stack4
  17     #define BASES private boost::contract::constructor_precondition<stack4<T> >
  18     : BASES
  19 {
  20     friend boost::contract::access;
  21     typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
  22     #undef BASES
  23
  24     void invariant() const {
  25         BOOST_CONTRACT_ASSERT(count() >= 0); // Count non-negative.
  26         BOOST_CONTRACT_ASSERT(count() <= capacity()); // Count bounded.
  27         BOOST_CONTRACT_ASSERT(empty() == (count() == 0)); // Empty if no elem.
  28     }
  29
  30 public:
  31     /* Initialization */
  32
  33     // Allocate static from a maximum of n elements.
  34     explicit stack4(int n) :
  35         boost::contract::constructor_precondition<stack4>([&] {
  36             BOOST_CONTRACT_ASSERT(n >= 0); // Non-negative capacity.
  37         })
  38     {
  39         boost::contract::check c = boost::contract::constructor(this)
  40             .postcondition([&] {
  41                 BOOST_CONTRACT_ASSERT(capacity() == n); // Capacity set.
  42             })
  43         ;
  44
  45         capacity_ = n;
  46         count_ = 0;
  47         array_ = new T[n];
  48     }
  49
  50     // Deep copy via constructor.
  51     /* implicit */ stack4(stack4 const& other) {
  52         boost::contract::check c = boost::contract::constructor(this)
  53             .postcondition([&] {
  54                 BOOST_CONTRACT_ASSERT(capacity() == other.capacity());
  55                 BOOST_CONTRACT_ASSERT(count() == other.count());
  56                 BOOST_CONTRACT_ASSERT_AXIOM(*this == other);
  57             })
  58         ;
  59
  60         capacity_ = other.capacity_;
  61         count_ = other.count_;
  62         array_ = new T[other.capacity_];
  63         for(int i = 0; i < other.count_; ++i) array_[i] = other.array_[i];
  64     }
  65
  66     // Deep copy via assignment.
  67     stack4& operator=(stack4 const& other) {
  68         boost::contract::check c = boost::contract::public_function(this)
  69             .postcondition([&] {
  70                 BOOST_CONTRACT_ASSERT(capacity() == other.capacity());
  71                 BOOST_CONTRACT_ASSERT(count() == other.count());
  72                 BOOST_CONTRACT_ASSERT_AXIOM(*this == other);
  73             })
  74         ;
  75
  76         delete[] array_;
  77         capacity_ = other.capacity_;
  78         count_ = other.count_;
  79         array_ = new T[other.capacity_];
  80         for(int i = 0; i < other.count_; ++i) array_[i] = other.array_[i];
  81         return *this;
  82     }
  83
  84     // Destroy this stack.
  85     virtual ~stack4() {
  86         // Check invariants.
  87         boost::contract::check c = boost::contract::destructor(this);
  88         delete[] array_;
  89     }
  90
  91     /* Access */
  92
  93     // Max number of stack elements.
  94     int capacity() const {
  95         // Check invariants.
  96         boost::contract::check c = boost::contract::public_function(this);
  97         return capacity_;
  98     }
  99
 100     // Number of stack elements.
 101     int count() const {
 102         // Check invariants.
 103         boost::contract::check c = boost::contract::public_function(this);
 104         return count_;
 105     }
 106
 107     // Top element.
 108     T const& item() const {
 109         boost::contract::check c = boost::contract::public_function(this)
 110             .precondition([&] {
 111                 BOOST_CONTRACT_ASSERT(!empty()); // Not empty (i.e., count > 0).
 112             })
 113         ;
 114
 115         return array_[count_ - 1];
 116     }
 117
 118     /* Status Report */
 119
 120     // Is stack empty?
 121     bool empty() const {
 122         bool result;
 123         boost::contract::check c = boost::contract::public_function(this)
 124             .postcondition([&] {
 125                 // Empty definition.
 126                 BOOST_CONTRACT_ASSERT(result == (count() == 0));
 127             })
 128         ;
 129
 130         return result = (count_ == 0);
 131     }
 132
 133     // Is stack full?
 134     bool full() const {
 135         bool result;
 136         boost::contract::check c = boost::contract::public_function(this)
 137             .postcondition([&] {
 138                 BOOST_CONTRACT_ASSERT( // Full definition.
 139                         result == (count() == capacity()));
 140             })
 141         ;
 142
 143         return result = (count_ == capacity_);
 144     }
 145
 146     /* Element Change */
 147
 148     // Add x on top.
 149     void put(T const& x) {
 150         boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
 151         boost::contract::check c = boost::contract::public_function(this)
 152             .precondition([&] {
 153                 BOOST_CONTRACT_ASSERT(!full()); // Not full.
 154             })
 155             .postcondition([&] {
 156                 BOOST_CONTRACT_ASSERT(!empty()); // Not empty.
 157                 BOOST_CONTRACT_ASSERT(item() == x); // Added to top.
 158                 BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // One more.
 159             })
 160         ;
 161
 162         array_[count_++] = x;
 163     }
 164
 165     // Remove top element.
 166     void remove() {
 167         boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
 168         boost::contract::check c = boost::contract::public_function(this)
 169             .precondition([&] {
 170                 BOOST_CONTRACT_ASSERT(!empty()); // Not empty (i.e., count > 0).
 171             })
 172             .postcondition([&] {
 173                 BOOST_CONTRACT_ASSERT(!full()); // Not full.
 174                 BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // One less.
 175             })
 176         ;
 177
 178         --count_;
 179     }
 180
 181     /* Friend Helpers */
 182
 183     friend bool operator==(stack4 const& left, stack4 const& right) {
 184         boost::contract::check inv1 = boost::contract::public_function(&left);
 185         boost::contract::check inv2 = boost::contract::public_function(&right);
 186         if(left.count_ != right.count_) return false;
 187         for(int i = 0; i < left.count_; ++i) {
 188             if(left.array_[i] != right.array_[i]) return false;
 189         }
 190         return true;
 191     }
 192
 193 private:
 194     int capacity_;
 195     int count_;
 196     T* array_; // Internally use C-style array.
 197 };
 198
 199 #endif // #include guard
 200 //]
 201