access.cpp 2.7 KB

1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495
  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 <cassert>
  8. template<typename T>
  9. class pushable {
  10. friend class boost::contract::access;
  11. void invariant() const {
  12. BOOST_CONTRACT_ASSERT(capacity() <= max_size());
  13. }
  14. public:
  15. virtual void push_back(T const& value, boost::contract::virtual_* v = 0)
  16. = 0;
  17. protected:
  18. virtual unsigned capacity() const = 0;
  19. virtual unsigned max_size() const = 0;
  20. };
  21. template<typename T>
  22. void pushable<T>::push_back(T const& value, boost::contract::virtual_* v) {
  23. boost::contract::old_ptr<unsigned> old_capacity =
  24. BOOST_CONTRACT_OLDOF(v, capacity());
  25. boost::contract::check c = boost::contract::public_function(v, this)
  26. .precondition([&] {
  27. BOOST_CONTRACT_ASSERT(capacity() < max_size());
  28. })
  29. .postcondition([&] {
  30. BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
  31. })
  32. ;
  33. assert(false);
  34. }
  35. //[access
  36. template<typename T>
  37. class vector
  38. #define BASES public pushable<T>
  39. : BASES
  40. { // Private section of the class.
  41. friend class boost::contract::access; // Friend `access` class so...
  42. typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // ...private bases.
  43. #undef BASES
  44. void invariant() const { // ...private invariants.
  45. BOOST_CONTRACT_ASSERT(size() <= capacity());
  46. }
  47. BOOST_CONTRACT_OVERRIDE(push_back) // ...private overrides.
  48. public: // Public section of the class.
  49. void push_back(T const& value, boost::contract::virtual_* v = 0)
  50. /* override */ {
  51. boost::contract::old_ptr<unsigned> old_size =
  52. BOOST_CONTRACT_OLDOF(v, size());
  53. boost::contract::check c = boost::contract::public_function<
  54. override_push_back>(v, &vector::push_back, this, value)
  55. .precondition([&] {
  56. BOOST_CONTRACT_ASSERT(size() < max_size());
  57. })
  58. .postcondition([&] {
  59. BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
  60. })
  61. ;
  62. vect_.push_back(value);
  63. }
  64. /* ... */
  65. //]
  66. unsigned size() const { return vect_.size(); }
  67. unsigned max_size() const { return vect_.max_size(); }
  68. unsigned capacity() const { return vect_.capacity(); }
  69. private: // Another private section.
  70. std::vector<T> vect_;
  71. };
  72. int main() {
  73. vector<int> vect;
  74. vect.push_back(123);
  75. assert(vect.size() == 1);
  76. return 0;
  77. }