stack3.cpp 5.9 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192
  1. // Copyright (C) 2008-2018 Lorenzo Caminiti
  2. // Distributed under the Boost Software License, Version 1.0 (see accompanying
  3. // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
  4. // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
  5. //[meyer97_stack3
  6. // File: stack3.cpp
  7. #include "stack4.hpp"
  8. #include <boost/contract.hpp>
  9. #include <boost/optional.hpp>
  10. #include <cassert>
  11. // Dispenser LIFO with max capacity using error codes.
  12. template<typename T>
  13. class stack3 {
  14. friend class boost::contract::access;
  15. void invariant() const {
  16. if(!error()) {
  17. BOOST_CONTRACT_ASSERT(count() >= 0); // Count non-negative.
  18. BOOST_CONTRACT_ASSERT(count() <= capacity()); // Count bounded.
  19. // Empty if no element.
  20. BOOST_CONTRACT_ASSERT(empty() == (count() == 0));
  21. }
  22. }
  23. public:
  24. enum error_code {
  25. no_error = 0,
  26. overflow_error,
  27. underflow_error,
  28. size_error
  29. };
  30. /* Initialization */
  31. // Create stack for max of n elems, if n < 0 set error (no preconditions).
  32. explicit stack3(int n, T const& default_value = T()) :
  33. stack_(0), error_(no_error) {
  34. boost::contract::check c = boost::contract::constructor(this)
  35. .postcondition([&] {
  36. // Error if impossible.
  37. BOOST_CONTRACT_ASSERT((n < 0) == (error() == size_error));
  38. // No error if possible.
  39. BOOST_CONTRACT_ASSERT((n >= 0) == !error());
  40. // Created if no error.
  41. if(!error()) BOOST_CONTRACT_ASSERT(capacity() == n);
  42. })
  43. ;
  44. if(n >= 0) stack_ = stack4<T>(n);
  45. else error_ = size_error;
  46. }
  47. /* Access */
  48. // Max number of stack elements.
  49. int capacity() const {
  50. // Check invariants.
  51. boost::contract::check c = boost::contract::public_function(this);
  52. return stack_.capacity();
  53. }
  54. // Number of stack elements.
  55. int count() const {
  56. // Check invariants.
  57. boost::contract::check c = boost::contract::public_function(this);
  58. return stack_.count();
  59. }
  60. // Top element if present, otherwise none and set error (no preconditions).
  61. boost::optional<T const&> item() const {
  62. boost::contract::check c = boost::contract::public_function(this)
  63. .postcondition([&] {
  64. // Error if impossible.
  65. BOOST_CONTRACT_ASSERT(empty() == (error() == underflow_error));
  66. // No error if possible.
  67. BOOST_CONTRACT_ASSERT(!empty() == !error());
  68. })
  69. ;
  70. if(!empty()) {
  71. error_ = no_error;
  72. return boost::optional<T const&>(stack_.item());
  73. } else {
  74. error_ = underflow_error;
  75. return boost::optional<T const&>();
  76. }
  77. }
  78. /* Status Report */
  79. // Error indicator set by various operations.
  80. error_code error() const {
  81. // Check invariants.
  82. boost::contract::check c = boost::contract::public_function(this);
  83. return error_;
  84. }
  85. bool empty() const {
  86. // Check invariants.
  87. boost::contract::check c = boost::contract::public_function(this);
  88. return stack_.empty();
  89. }
  90. bool full() const {
  91. // Check invariants.
  92. boost::contract::check c = boost::contract::public_function(this);
  93. return stack_.full();
  94. }
  95. /* Element Change */
  96. // Add x to top if capacity allows, otherwise set error (no preconditions).
  97. void put(T const& x) {
  98. boost::contract::old_ptr<bool> old_full = BOOST_CONTRACT_OLDOF(full());
  99. boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
  100. boost::contract::check c = boost::contract::public_function(this)
  101. .postcondition([&] {
  102. // Error if impossible.
  103. BOOST_CONTRACT_ASSERT(*old_full == (error() == overflow_error));
  104. // No error if possible.
  105. BOOST_CONTRACT_ASSERT(!*old_full == !error());
  106. if(!error()) { // If no error...
  107. BOOST_CONTRACT_ASSERT(!empty()); // ...not empty.
  108. BOOST_CONTRACT_ASSERT(*item() == x); // ...added to top.
  109. // ...one more.
  110. BOOST_CONTRACT_ASSERT(count() == *old_count + 1);
  111. }
  112. })
  113. ;
  114. if(full()) error_ = overflow_error;
  115. else {
  116. stack_.put(x);
  117. error_ = no_error;
  118. }
  119. }
  120. // Remove top element if possible, otherwise set error (no preconditions).
  121. void remove() {
  122. boost::contract::old_ptr<bool> old_empty =
  123. BOOST_CONTRACT_OLDOF(empty());
  124. boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
  125. boost::contract::check c = boost::contract::public_function(this)
  126. .postcondition([&] {
  127. // Error if impossible.
  128. BOOST_CONTRACT_ASSERT(*old_empty == (error() ==
  129. underflow_error));
  130. // No error if possible.
  131. BOOST_CONTRACT_ASSERT(!*old_empty == !error());
  132. if(!error()) { // If no error...
  133. BOOST_CONTRACT_ASSERT(!full()); // ...not full.
  134. // ...one less.
  135. BOOST_CONTRACT_ASSERT(count() == *old_count - 1);
  136. }
  137. })
  138. ;
  139. if(empty()) error_ = underflow_error;
  140. else {
  141. stack_.remove();
  142. error_ = no_error;
  143. }
  144. }
  145. private:
  146. stack4<T> stack_;
  147. mutable error_code error_;
  148. };
  149. int main() {
  150. stack3<int> s(3);
  151. assert(s.capacity() == 3);
  152. assert(s.count() == 0);
  153. assert(s.empty());
  154. assert(!s.full());
  155. s.put(123);
  156. assert(!s.empty());
  157. assert(!s.full());
  158. assert(*s.item() == 123);
  159. s.remove();
  160. assert(s.empty());
  161. assert(!s.full());
  162. return 0;
  163. }
  164. //]