Re: [boost] [contract] extra type requirements for contracts

Subject: Re: [boost] [contract] extra type requirements for contracts
From: lcaminiti (lorcaminiti_at_[hidden])
Date: 2011-09-29 12:49:14

lcaminiti wrote:
> 
> A possible solution is to specify the type requirements that a given
> assertion introduces. If the type requirements are met, the assertion will
> be compiled and checked at run-time. If the type requirements are not met,
> the assertion will not be compiled (so not compiler-error "missing
> operator== for type ...") and not checked at run-time for that specific
> type. For example:
> 

Hello all,

This is how assertion requirements implementation turned out to be (many
thanks again to everyone and especially to Andrzej Krzemienski for your
suggestions):

#include <contract.hpp>
#include &lt;boost/type_traits/can_call_equal.hpp&gt;
#include &lt;boost/type_traits/can_call_greater.hpp&gt;
#include &lt;boost/concept_check.hpp&gt;
#include &lt;boost/utility.hpp&gt;
#include <iostream>

template< typename T >
class PreIncrementable {
    T& x;
    void return_type ( T& );
public:
    BOOST_CONCEPT_USAGE(PreIncrementable) {
        return_type(++x);
    }
};

CONTRACT_FUNCTION(
template( typename T ) requires( PreIncrementable<T> )
(T&) (inc) ( (T&) value )
    postcondition(
        auto result = return,
        // skip this old-of copy if `has_oldof<T>::value` is false
        auto old_value = CONTRACT_OLDOF value,
        // skip this assertion if `has_oldof<T>::value` is false
        value > old_value, // also skip if T has no operator>
                requires contract::has_oldof<T>::value &&   // need old-of
                         boost::can_call_greater<T>::value, // need >
        result == value, // skip this assertion if T has no operator==
                requires boost::can_call_equal<T>::value    // need ==
    )
) {
    return ++value;
}

struct counter : boost::noncopyable { // cannot copy (for some reason...)
    counter ( ) : number_(0) {}

    counter& operator++ ( ) { ++number_; return *this; }

    friend bool operator> ( counter const& left, counter const& right )
        { return left.number_ > right.number_; }
    
    void print ( ) { std::cout << number_ << std::endl; }

private:
    int number_;
};

// specialization disables old-of for non-copyable `counter` (no type trait
can
// be implemented in C++ to automatically and portably detect copy
constructor)
namespace contract {
    template<> struct has_oldof<counter> : boost::mpl::false_ {};
}

int main ( ) {
    int i = 0;
    std::cout << inc(i) << std::endl; // check entire contract for `int`
type

    counter c;
    inc(c).print(); // cannot copy `counter` so skip assertion with old-of
    return 0;
}

Unfortunately, some extra work is required by the users to deal with old-of
-- they need to specialize has_oldof. This is because there is no type trait
that can check if a type T has a const-correct copy constructor (portably
and also including user-defined copy constructors) so I was forced to
trivially inherit has_oldof<T> from mpl::true_ (this way contract
compilation will fail for types without a const-correct copy constructor and
in this case programmers can specialize has_oldof to inherit from false_ to
disable the old-of assertions and compile the code as in the example above).
To be precise, my library copies old-of using a copy<> template which by
default looks for a const-correct copy constructor. So users have full
control even if they want old-of for a type that cannot define a
const-correct copy constructor by specializing both copy<> and has_oldof<>
(but this is a rather advanced use of the library and it is probably never
needed).

All of that said, usually old-of copies are takes for counters or iterators
so you don't even have to worry about specifying the has_oldof requirements
in the contracts (let alone specializing has_oldof) because these types will
always be copyable.

--Lorenzo

--
View this message in context: http://boost.2283326.n4.nabble.com/boost-contract-extra-type-requirements-for-contracts-tp3824535p3856647.html
Sent from the Boost - Dev mailing list archive at Nabble.com.