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 13:30:14

Vicente Botet wrote:
> 
> 
> 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.
> 

I think this can be achieved with my previous "option 2" suggestion:

namespace dummy {
    template< typename L, typename R>
    bool operator== ( L const&, R const& ) { return true; }
}

postcondition(
    using dummy::operator==,
    back() == value
)

This will use T's operator== if there is one, otherwise it will use
operator== from the dummy namespace. You can defined/overload the
dummy::operator== as you wish (Boost.Contract might even provide a few of
such dummy operators as contract::trivial::operator==,
contract::trivial::operator<, etc). There is no need for the macros to do
anything special here.

However, option 2 deals well with the (most common) issue of operator== but
it doesn't handle the general issue that an assertion might introduce an
arbitrary extra set of type requirements on generic types (e.g., == and +
and copyable and ...). So I want to also implement option 1 "assertions with
type requirements" 

P.S. Plus I think I can use option 1 to also implement assertion importance
ordering and therefore remove the "importance" keyword:

// Use importance ordering (in assertion requirements) to model
computational complexity.
#define O_1 0 // O(1)
#define O_N 1 // O(n)

#define COMPLEXITY_MAX O_1 // Only check assertions with constant
complexity.

postcondition(
    auto result = return,
    result == *(std::find(v.begin(), v.end(), value)),
            requires O_N <= COMPLEXITY_MAX && has_equal_to<T>::value
)

Thanks.
--Lorenzo

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