123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213 |
- // Copyright (C) 2008-2018 Lorenzo Caminiti
- // Distributed under the Boost Software License, Version 1.0 (see accompanying
- // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
- // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
- #include <vector>
- #include <limits>
- #include <cassert>
- //[ifdef_function
- // Use #ifdef to completely disable contract code compilation.
- #include <boost/contract/core/config.hpp>
- #ifndef BOOST_CONTRACT_NO_ALL
- #include <boost/contract.hpp>
- #endif
- int inc(int& x) {
- int result;
- #ifndef BOOST_CONTRACT_NO_OLDS
- boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x);
- #endif
- #ifndef BOOST_CONTRACT_NO_FUNCTIONS
- boost::contract::check c = boost::contract::function()
- #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
- .precondition([&] {
- BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max());
- })
- #endif
- #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
- .postcondition([&] {
- BOOST_CONTRACT_ASSERT(x == *old_x + 1);
- BOOST_CONTRACT_ASSERT(result == *old_x);
- })
- #endif
- ;
- #endif
- return result = x++;
- }
- //]
- template<typename T>
- class pushable {
- #ifndef BOOST_CONTRACT_NO_ALL
- friend class boost::contract::access;
- #endif
- #ifndef BOOST_CONTRACT_NO_INVARIANTS
- void invariant() const {
- BOOST_CONTRACT_ASSERT(capacity() <= max_size());
- }
- #endif
- public:
- virtual void push_back(
- T const& x
- #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
- , boost::contract::virtual_* v = 0
- #endif
- ) = 0;
- protected:
- virtual unsigned capacity() const = 0;
- virtual unsigned max_size() const = 0;
- };
- template<typename T>
- void pushable<T>::push_back(
- T const& x
- #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
- , boost::contract::virtual_* v
- #endif
- ) {
- #ifndef BOOST_CONTRACT_NO_OLDS
- boost::contract::old_ptr<unsigned> old_capacity =
- BOOST_CONTRACT_OLDOF(v, capacity());
- #endif
- #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
- boost::contract::check c = boost::contract::public_function(v, this)
- #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
- .precondition([&] {
- BOOST_CONTRACT_ASSERT(capacity() < max_size());
- })
- #endif
- #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
- .postcondition([&] {
- BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
- })
- #endif
- ;
- #endif
- assert(false); // Shall never execute this body.
- }
- //[ifdef_class
- class integers
- #define BASES public pushable<int>
- :
- #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
- private boost::contract::constructor_precondition<integers>, BASES
- #else
- BASES
- #endif
- {
- #ifndef BOOST_CONTRACT_NO_ALL
- friend class boost::contract::access;
- #endif
- #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
- typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
- #endif
- #undef BASES
- #ifndef BOOST_CONTRACT_NO_INVARIANTS
- void invariant() const {
- BOOST_CONTRACT_ASSERT(size() <= capacity());
- }
- #endif
- public:
- integers(int from, int to) :
- #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
- boost::contract::constructor_precondition<integers>([&] {
- BOOST_CONTRACT_ASSERT(from <= to);
- }),
- #endif
- vect_(to - from + 1)
- {
- #ifndef BOOST_CONTRACT_NO_CONSTRUCTORS
- boost::contract::check c = boost::contract::constructor(this)
- #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
- .postcondition([&] {
- BOOST_CONTRACT_ASSERT(int(size()) == (to - from + 1));
- })
- #endif
- ;
- #endif
- for(int x = from; x <= to; ++x) vect_.at(x - from) = x;
- }
-
- virtual ~integers() {
- #ifndef BOOST_CONTRACT_NO_DESTRUCTORS
- // Check invariants.
- boost::contract::check c = boost::contract::destructor(this);
- #endif
- }
- virtual void push_back(
- int const& x
- #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
- , boost::contract::virtual_* v = 0
- #endif
- ) /* override */ {
- #ifndef BOOST_CONTRACT_NO_OLDS
- boost::contract::old_ptr<unsigned> old_size;
- #endif
- #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
- boost::contract::check c = boost::contract::public_function<
- override_push_back>(v, &integers::push_back, this, x)
- #ifndef BOOST_CONTRACT_NO_PRECONDITIONS
- .precondition([&] {
- BOOST_CONTRACT_ASSERT(size() < max_size());
- })
- #endif
- #ifndef BOOST_CONTRACT_NO_OLDS
- .old([&] {
- old_size = BOOST_CONTRACT_OLDOF(v, size());
- })
- #endif
- #ifndef BOOST_CONTRACT_NO_POSTCONDITIONS
- .postcondition([&] {
- BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
- })
- #endif
- #ifndef BOOST_CONTRACT_NO_EXCEPTS
- .except([&] {
- BOOST_CONTRACT_ASSERT(size() == *old_size);
- })
- #endif
- ;
- #endif
- vect_.push_back(x);
- }
- private:
- #ifndef BOOST_CONTRACT_NO_PUBLIC_FUNCTIONS
- BOOST_CONTRACT_OVERRIDE(push_back)
- #endif
- /* ... */
- //]
- public: // Could program contracts for these too...
- unsigned size() const { return vect_.size(); }
- unsigned max_size() const { return vect_.max_size(); }
- unsigned capacity() const { return vect_.capacity(); }
- private:
- std::vector<int> vect_;
- };
- int main() {
- integers i(1, 10);
- int x = 123;
- i.push_back(inc(x));
- assert(x == 124);
- assert(i.size() == 11);
- return 0;
- }
|