public.cpp 5.6 KB

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