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

Subject: Re: [boost] [contract] extra type requirements for contracts
From: Vicente Botet (vicente.botet_at_[hidden])
Date: 2011-09-22 12:00:16

lcaminiti wrote:
> 
> 
> 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
> 

Hi,

I think you can provide something simpler. Instead of writing the enabling
condition maybe you can
use an intermediary function. In your case instead of using directly back()
== value you can use

are_equivalents(back(),value)

this function can be defined to use back() == value when
boost::can_call_equal. The default definition could be to return true or
just don't define it at all and let the user make the specialization.

I guess that your macros could replace these automatically, so the user
could continue to use back() == value.

Best,
Vicente

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