libs/contract/example/features/access.cpp

   1
   2 // Copyright (C) 2008-2018 Lorenzo Caminiti
   3 // Distributed under the Boost Software License, Version 1.0 (see accompanying
   4 // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
   5 // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
   6
   7 #include <boost/contract.hpp>
   8 #include <vector>
   9 #include <cassert>
  10
  11 template<typename T>
  12 class pushable {
  13     friend class boost::contract::access;
  14
  15     void invariant() const {
  16         BOOST_CONTRACT_ASSERT(capacity() <= max_size());
  17     }
  18
  19 public:
  20     virtual void push_back(T const& value, boost::contract::virtual_* v = 0)
  21             = 0;
  22
  23 protected:
  24     virtual unsigned capacity() const = 0;
  25     virtual unsigned max_size() const = 0;
  26 };
  27
  28 template<typename T>
  29 void pushable<T>::push_back(T const& value, boost::contract::virtual_* v) {
  30     boost::contract::old_ptr<unsigned> old_capacity =
  31             BOOST_CONTRACT_OLDOF(v, capacity());
  32     boost::contract::check c = boost::contract::public_function(v, this)
  33         .precondition([&] {
  34             BOOST_CONTRACT_ASSERT(capacity() < max_size());
  35         })
  36         .postcondition([&] {
  37             BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
  38         })
  39     ;
  40     assert(false);
  41 }
  42
  43 //[access
  44 template<typename T>
  45 class vector
  46     #define BASES public pushable<T>
  47     : BASES
  48 { // Private section of the class.
  49     friend class boost::contract::access; // Friend `access` class so...
  50
  51     typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // ...private bases.
  52     #undef BASES
  53
  54     void invariant() const { // ...private invariants.
  55         BOOST_CONTRACT_ASSERT(size() <= capacity());
  56     }
  57
  58     BOOST_CONTRACT_OVERRIDE(push_back) // ...private overrides.
  59
  60 public: // Public section of the class.
  61     void push_back(T const& value, boost::contract::virtual_* v = 0)
  62             /* override */ {
  63         boost::contract::old_ptr<unsigned> old_size =
  64                 BOOST_CONTRACT_OLDOF(v, size());
  65         boost::contract::check c = boost::contract::public_function<
  66                 override_push_back>(v, &vector::push_back, this, value)
  67             .precondition([&] {
  68                 BOOST_CONTRACT_ASSERT(size() < max_size());
  69             })
  70             .postcondition([&] {
  71                 BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
  72             })
  73         ;
  74
  75         vect_.push_back(value);
  76     }
  77
  78     /* ... */
  79 //]
  80
  81     unsigned size() const { return vect_.size(); }
  82     unsigned max_size() const { return vect_.max_size(); }
  83     unsigned capacity() const { return vect_.capacity(); }
  84
  85 private: // Another private section.
  86     std::vector<T> vect_;
  87 };
  88
  89 int main() {
  90     vector<int> vect;
  91     vect.push_back(123);
  92     assert(vect.size() == 1);
  93     return 0;
  94 }
  95