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-22 11:03:09

lcaminiti wrote:
> 
> 
> Dave Abrahams wrote:
>> 
>> on Tue Sep 20 2011, lcaminiti <lorcaminiti-AT-gmail.com> wrote:
>> 
>>> Dave Abrahams wrote:
>>>> 
>>>
>>>> on Mon Sep 19 2011, lcaminiti <lorcaminiti-AT-gmail.com> wrote:
>>>> 
>>>>> This is a general issue with contracts. In general, an arbitrary
>>>>> complex
>>>>> (const) expression can be used to assert preconditions,
>>>>> postconditions,
>>>>> or
>>>>> invariants. Such a complex assertion might introduce an arbitray set
>>>>> of
>>>>> extra requirements on the types used, requirements that might not be
>>>>> necessary to implement the function body. The extra type requirements
>>>>> introduced by the contracts are especially problematic when
>>>>> programming
>>>>> templates because the used types are generic and it is not know a
>>>>> priori
>>>>> to
>>>>> the function programmer if the generic types will or not satisfy the
>>>>> requirements.
>>>> 
>>>> If the contract can't be expressed within the constraints, the
>>>> constraints are broken, period.
>>>
>>> But this means that if you add contracts to vector<T> then you cannot
>>> use it unless T is EqualityComparable...  I don't think that will be
>>> acceptable to Boost.Contract users... will it be acceptable?
>> 
>> No, almost certainly not.
>> 
>> It would probably be reasonable to say that *if* T supports ==, the
>> contract checking will use that, and otherwise, the parts of the
>> contract that depend on == won't be checked.
>> 
> 
> Yes, this is exactly what the assertion type requirement idea tries to do:
> 
> CONTRACT_FUNCTION_TPL( // option 1
> public void (push_back) ( (T const&) value)
>     postcondition(
>         back() == value, requires has_equal_to<T>::value
>     )
> ) ;
> 
> Here the assertion `back() == value` is compiled and checked if and only
> if its requirement `has_equal_to<T>::value` is true for T.
> 

Hello all,

I am trying to program an assertion that is compiled and checked at run-time
only when an integral boolean expression expressing the assertion
requirements is true.

For example, the following code asserts back() == value only when
can_call_equal<T>::value is true. However, is there a better way to do this
that does not require the extra function call to post1?

#include &lt;boost/mpl/bool.hpp&gt;
#include &lt;boost/type_traits/can_call_equal.hpp&gt;
#include <vector>
#include <cassert>
#include <iostream>

template< typename T >
struct myvector {

//  CONTRACT_FUNCTION_TPL(
//  public void (push_back) ( (T const&) value )
//      postcondition(
//          back() == value, requires boost::can_call_equal<T>::value
//      )
//  ) { vector_.push_back(value); }

    void post1 ( boost::mpl::true_, T const& value ) const {
        std::clog << "actual assertion\n";
        assert( /**/ back() == value /**/ );
    }
    void post1 ( boost::mpl::false_, T const& value ) const {
        std::clog << "trivial assertion\n";
    }
    void push_back ( T const& value ) {
        body(value);
        post1(typename boost::mpl::bool_<
                /**/ boost::can_call_equal<T>::value /**/ >::type(),
                value);
    }
    void body ( T const& value )
        /**/ { vector_.push_back(value); } /**/

    T const& back ( void ) const { return vector_.back(); }

private:
    std::vector<T> vector_;
};

struct pod {};

int main ( ) {
    myvector<int> v;
    std::clog << "push 123\n";
    v.push_back(123);

    myvector<pod> w;
    std::clog << "push POD\n";
    w.push_back(pod());
    return 0;
}

Note that post1(boost::mpl::true_, ...) is not even compiled for
myvector<pod> and that is essential because such a compilation attempt will
fail because pod does not have an operator==.

Thanks a lot for any suggestion you might have.
--Lorenzo

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