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-20 13:23:16

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.

> Another reasonable possibility (which could be used together with the
> former one) would be to provide a hook for people to implement some
> equivalence test for T that isn't spelled "==".  That said, I would
> argue that if they can implement the equivalence test, they should call
> it "==".
> 

Yes, this is what I have currently implemented:

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

CONTRACT_FUNCTION_TPL( // option 2
public void (push_back) ( (T const&) value)
    postcondition(
        using dummy::operator==,
        back() == value
    )
) ;

This will use the dummy implementation of operator== only when T does not
already have a better match for operator==. Boost.Contract could in fact
provide a bunch of dummy operator implementations as
contract::trivial::operator==, contract::trivial::operator<, etc. The
implementation doesn't have to be dummy, with this method you can actually
program a special operator== that does something and to be used by the
contract only when T does not already have an operator==.

(Note that contracts can safely allow using directives, namespace aliasing,
typedefs, etc because these are all constant correct operations as they do
not change the program's run-time state.)

> Overall I have more confidence in the first idea above than in the
> second one.
> 

I like option 1 better than option 2 because option 1 is more general while
option 2 only handles the == case (and some other predefined operations like
<, etc). What do you think?

>>> Now, however, the standard contains special hand-wavey language that
>>> says, essentially, "when we use a == b to describe a postcondition we
>>> don't literally mean ==.  We mean that a and b are equivalent" (whatever
>>> that means).  So even if T supports == it doesn't necessarily mean the
>>> standard is going to use it.  I think what it really means is that b is
>>> indistinguishable from any other copy of a.
>>> 
>>> ...which doesn't help you at all in terms of deciding what to actually
>>> /do/, I know... hopefully, though, it muddies the water a bit just in
>>> case it was too clear for you up till now ;-)
>>> 
>>
>> I will study this part of the standard.
> 
> Good luck.
> 
> Incidentally, this is part of the reason Stepanov puts so much emphasis
> on the importance of "regular types:" you can't check (programmatically
> or by inspection) even the most basic assertions about the correctness
> of code that copies data unless you have some notion of "==" for just
> 

I think that's why Eiffel does not address the extra type requirement issue
because (AFAIK) you can always compare Eiffel's types for equality.

> about everything.  However, the C++ standard was written to accomodate
> "partial" types that lack essential operations, so what are you gonna
> do?
> 

Because Boost.Contract implements Contract Programming for C++, I must deal
with the partial types that the C++ standards allows... so I think I will
implement option 1 (or option 2) and document that if you don't provide
meaningful == most of your assertions (especially postconditions) won't be
checked.

Thanks a lot!
--Lorenzo

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