introduction_public.cpp 2.8 KB

1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889
  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 { // Somewhat arbitrary base (used just to show subcontracting).
  10. public:
  11. void invariant() const {
  12. BOOST_CONTRACT_ASSERT(capacity() <= max_size());
  13. }
  14. virtual void push_back(T const& value,
  15. boost::contract::virtual_* v = 0) = 0; // Pure virtual function.
  16. protected:
  17. virtual unsigned capacity() const = 0;
  18. virtual unsigned max_size() const = 0;
  19. };
  20. template<typename T> // Contract for pure virtual function.
  21. void pushable<T>::push_back(T const& value, boost::contract::virtual_* v) {
  22. boost::contract::old_ptr<unsigned> old_capacity =
  23. BOOST_CONTRACT_OLDOF(v, capacity());
  24. boost::contract::check c = boost::contract::public_function(v, this)
  25. .precondition([&] {
  26. BOOST_CONTRACT_ASSERT(capacity() < max_size());
  27. })
  28. .postcondition([&] {
  29. BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
  30. })
  31. ;
  32. assert(false); // Shall never execute this body.
  33. }
  34. //[introduction_public
  35. template<typename T>
  36. class vector
  37. #define BASES public pushable<T>
  38. : BASES
  39. {
  40. public:
  41. typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // For subcontracting.
  42. #undef BASES
  43. void invariant() const { // Checked in AND with base class invariants.
  44. BOOST_CONTRACT_ASSERT(size() <= capacity());
  45. }
  46. virtual void push_back(T const& value,
  47. boost::contract::virtual_* v = 0) /* override */ { // For virtuals.
  48. boost::contract::old_ptr<unsigned> old_size =
  49. BOOST_CONTRACT_OLDOF(v, size()); // Old values for virtuals.
  50. boost::contract::check c = boost::contract::public_function< // For overrides.
  51. override_push_back>(v, &vector::push_back, this, value)
  52. .precondition([&] { // Checked in OR with base preconditions.
  53. BOOST_CONTRACT_ASSERT(size() < max_size());
  54. })
  55. .postcondition([&] { // Checked in AND with base postconditions.
  56. BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
  57. })
  58. ;
  59. vect_.push_back(value);
  60. }
  61. BOOST_CONTRACT_OVERRIDE(push_back) // Define `override_push_back` above.
  62. // Could program contracts for those as well.
  63. unsigned size() const { return vect_.size(); }
  64. unsigned max_size() const { return vect_.max_size(); }
  65. unsigned capacity() const { return vect_.capacity(); }
  66. private:
  67. std::vector<T> vect_;
  68. };
  69. //]
  70. int main() {
  71. vector<int> vect;
  72. vect.push_back(123);
  73. assert(vect.size() == 1);
  74. return 0;
  75. }