simple_queue.cpp 6.6 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219
  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. //[mitchell02_simple_queue
  6. #include <boost/contract.hpp>
  7. #include <boost/optional.hpp>
  8. #include <vector>
  9. #include <cassert>
  10. template<typename T>
  11. class simple_queue
  12. #define BASES private boost::contract::constructor_precondition< \
  13. simple_queue<T> >
  14. : BASES
  15. {
  16. friend class boost::contract::access;
  17. typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
  18. #undef BASES
  19. void invariant() const {
  20. BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
  21. }
  22. public:
  23. /* Creation */
  24. // Create empty queue.
  25. explicit simple_queue(int a_capacity) :
  26. boost::contract::constructor_precondition<simple_queue>([&] {
  27. BOOST_CONTRACT_ASSERT(a_capacity > 0); // Positive capacity.
  28. })
  29. {
  30. boost::contract::check c = boost::contract::constructor(this)
  31. .postcondition([&] {
  32. // Capacity set.
  33. BOOST_CONTRACT_ASSERT(capacity() == a_capacity);
  34. BOOST_CONTRACT_ASSERT(is_empty()); // Empty.
  35. })
  36. ;
  37. items_.reserve(a_capacity);
  38. }
  39. // Destroy queue.
  40. virtual ~simple_queue() {
  41. // Check invariants.
  42. boost::contract::check c = boost::contract::destructor(this);
  43. }
  44. /* Basic Queries */
  45. // Items in queue (in their order).
  46. // (Somewhat exposes implementation but allows to check more contracts.)
  47. std::vector<T> const& items() const {
  48. // Check invariants.
  49. boost::contract::check c = boost::contract::public_function(this);
  50. return items_;
  51. }
  52. // Max number of items queue can hold.
  53. int capacity() const {
  54. // Check invariants.
  55. boost::contract::check c = boost::contract::public_function(this);
  56. return items_.capacity();
  57. }
  58. /* Derived Queries */
  59. // Number of items.
  60. int count() const {
  61. int result;
  62. boost::contract::check c = boost::contract::public_function(this)
  63. .postcondition([&] {
  64. // Return items count.
  65. BOOST_CONTRACT_ASSERT(result == int(items().size()));
  66. })
  67. ;
  68. return result = items_.size();
  69. }
  70. // Item at head.
  71. T const& head() const {
  72. boost::optional<T const&> result;
  73. boost::contract::check c = boost::contract::public_function(this)
  74. .precondition([&] {
  75. BOOST_CONTRACT_ASSERT(!is_empty()); // Not empty.
  76. })
  77. .postcondition([&] {
  78. // Return item on top.
  79. BOOST_CONTRACT_ASSERT(*result == items().at(0));
  80. })
  81. ;
  82. return *(result = items_.at(0));
  83. }
  84. // If queue contains no item.
  85. bool is_empty() const {
  86. bool result;
  87. boost::contract::check c = boost::contract::public_function(this)
  88. .postcondition([&] {
  89. // Consistent with count.
  90. BOOST_CONTRACT_ASSERT(result == (count() == 0));
  91. })
  92. ;
  93. return result = (items_.size() == 0);
  94. }
  95. // If queue has no room for another item.
  96. bool is_full() const {
  97. bool result;
  98. boost::contract::check c = boost::contract::public_function(this)
  99. .postcondition([&] {
  100. BOOST_CONTRACT_ASSERT( // Consistent with size and capacity.
  101. result == (capacity() == int(items().size())));
  102. })
  103. ;
  104. return result = (items_.size() == items_.capacity());
  105. }
  106. /* Commands */
  107. // Remove head itme and shift all other items.
  108. void remove() {
  109. // Expensive all_equal postcond. and old_items copy might be skipped.
  110. boost::contract::old_ptr<std::vector<T> > old_items;
  111. #ifdef BOOST_CONTRACT_AUDIITS
  112. = BOOST_CONTRACT_OLDOF(items())
  113. #endif // Else, leave old pointer null...
  114. ;
  115. boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
  116. boost::contract::check c = boost::contract::public_function(this)
  117. .precondition([&] {
  118. BOOST_CONTRACT_ASSERT(!is_empty()); // Not empty.
  119. })
  120. .postcondition([&] {
  121. BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec.
  122. // ...following skipped #ifndef AUDITS.
  123. if(old_items) all_equal(items(), *old_items, /* shifted = */ 1);
  124. })
  125. ;
  126. items_.erase(items_.begin());
  127. }
  128. // Add item to tail.
  129. void put(T const& item) {
  130. // Expensive all_equal postcond. and old_items copy might be skipped.
  131. boost::contract::old_ptr<std::vector<T> > old_items;
  132. #ifdef BOOST_CONTRACT_AUDITS
  133. = BOOST_CONTRACT_OLDOF(items())
  134. #endif // Else, leave old pointer null...
  135. ;
  136. boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
  137. boost::contract::check c = boost::contract::public_function(this)
  138. .precondition([&] {
  139. BOOST_CONTRACT_ASSERT(count() < capacity()); // Room for add.
  140. })
  141. .postcondition([&] {
  142. BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc.
  143. // Second to last item.
  144. BOOST_CONTRACT_ASSERT(items().at(count() - 1) == item);
  145. // ...following skipped #ifndef AUDITS.
  146. if(old_items) all_equal(items(), *old_items);
  147. })
  148. ;
  149. items_.push_back(item);
  150. }
  151. private:
  152. // Contract helper.
  153. static bool all_equal(std::vector<T> const& left,
  154. std::vector<T> const& right, unsigned offset = 0) {
  155. boost::contract::check c = boost::contract::function()
  156. .precondition([&] {
  157. // Correct offset.
  158. BOOST_CONTRACT_ASSERT(right.size() == left.size() + offset);
  159. })
  160. ;
  161. for(unsigned i = offset; i < right.size(); ++i) {
  162. if(left.at(i - offset) != right.at(i)) return false;
  163. }
  164. return true;
  165. }
  166. std::vector<T> items_;
  167. };
  168. int main() {
  169. simple_queue<int> q(10);
  170. q.put(123);
  171. q.put(456);
  172. assert(q.capacity() == 10);
  173. assert(q.head() == 123);
  174. assert(!q.is_empty());
  175. assert(!q.is_full());
  176. std::vector<int> const& items = q.items();
  177. assert(items.at(0) == 123);
  178. assert(items.at(1) == 456);
  179. q.remove();
  180. assert(q.count() == 1);
  181. return 0;
  182. }
  183. //]