[boost] [contract] extra type requirements for contracts

classic Classic list List threaded Threaded
20 messages Options
Reply | Threaded
Open this post in threaded view
|

[boost] [contract] extra type requirements for contracts

lcaminiti
Hello all,

Andrzej and I have been discussing off-line the following issue:

    How to program contract assertions without adding extra type requirements.

I would like to get Boosters' input on possible solutions for this problem.

THE PROBLEM

Consider the following contract for vector::push_back:

CONTRACT_CLASS(
template( typename T )
class (myvector)
) {
    ...

    CONTRACT_FUNCTION_TPL(
    public void (push_back) ( (const T&) value )
        precondition(
            size() < max_size(),
        )
        postcondition(
            auto old_size = CONTRACT_OLDOF size(),
            auto old_capacity = CONTRACT_OLDOF capacity(),
            back() == value, // (1)
            size() == old_size + 1,
            capacity() >= old_capacity,
        )
    ) ;
};

Postcondition (1) introduces the extra requirement EqualityComparable<T>. This is not ideal because this requirement is only needed to check the contract but not to implement the push_back functionality (body). For example:

struct pod {}; // not EqualityComparable

std::vector<pod> v;
v.push_back(pod()); // ok, does not require EqualityComparable<pod>

myvector<pod> w;
w.push_back(pod()); // complier-error, can't find operator== for type pod...

Because of postcondition (1), myvector cannot be used on pod while the std::vector can!

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.

POSSIBLE SOLUTIONS

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:

    CONTRACT_FUNCTION_TPL( // Option 1
    public void (push_back) ( (const T&) value )
        precondition(
            size() < max_size(), requires has_less<size_type>::value
        )
        postcondition(
            auto old_size = CONTRACT_OLDOF size(),
                    requires const_copy_constructor<size_type>::value
            auto old_capacity = CONTRACT_OLDOF capacity(),
                    requires const_copy_constructor<size_type>::value
            back() == value, requires has_equal_to<T>::value // assertion type requirements
            size() == old_size + 1,
                    requires has_equal_to<size_type>::value &&
                             has_plus<size_type>::value
            capacity() >= old_capacity,
                    requires has_greater_equal<size_type>::value
        )
    ) ;

Here I have specified assertion type requirements using `requires` for each assertion. However, size_type is known a priori to be essentially an unsigned int for which all these type requirements will always be met so the type requirements on size_type could have been omitted. That said, you can easily imagine an example for a different template class or function where size_type is also a generic type for which const copy constructor, +, ==, etc might not always be available.

Another option would be would be to specify the type requirements for precondition/postcondition instead than for each assertion:

    CONTRACT_FUNCTION_TPL( // Option 2.
    public void (push_back) ( (const T&) value )
        precondition(
            size() < max_size(),
        ) requires has_less<size_type>::value // pre/postcondition type requirements
        postcondition(
            auto old_size = CONTRACT_OLDOF size(),
            auto old_capacity = CONTRACT_OLDOF capacity(),
            back() == value,
            size() == old_size + 1,
            capacity() >= old_capacity,
        ) requires
                const_copy_constructor<size_type>::value &&
                has_equal_to<T>::value &&
                has_plus<size_type>::value &&
                has_greater_equal<size_type>::value
    ) ;

Options 2 is less verbose and it does not specify the same type requirements multiple time for the different assertions. However, I prefer Option 1 because if T is not equality comparable, only the postcondition `back() == value` is not checked but all the other postconditions are still checked. With Option 2 if one type requirement is not met, then all preconditions/postconditions are not checked causing more bugs to go unobserved.

If the re-use of the preprocessor "keyword" `requires` was found confusing because of its different semantics when used with concepts, a different preprocessor "keyword" like `unless` could be used instead:

CONTRACT_FUNCTION( // Option 3
template( typename InIter1, typename InIter2, typename OutIter, typename BinOp )
    requires(
        boost::InputIterator<InIter1>,
        boost::InputIterator<InIter2>,
        typename CONTRACT_IDENTITY_TYPE(( boost::OutputIterator<OutIter,
                typename boost::InputIterator<InIter1>::value_type > )),
        typename CONTRACT_IDENTITY_TYPE(( boost::BinaryFunction<BinOp,
                typename boost::InputIterator<InIter1>::value_type,
                typename boost::InputIterator<InIter1>::value_type,
                typename boost::InputIterator<InIter2>::value_type> ))
    )
(OutIter) (mytransform) ( (InIter1) first1, (InIter1) last1, (InIter2) first2,
        (OutIter) result, (BinOp) op )
    precondition( contract::trivial::range(first1, last1).valid() )
    postcondition(
        auto return_value = return,
        return_value == result, unless !has_equal_to<T>::value // use unless
    )
) {
    return std::transform(first1, last1, first2, result, op);
}

Reflections:
a) All these solutions require extensive type traits support to write the contract type requirements (I cannot use concepts because they greedily generate compiler-errors when they are not met). However, I see no way around this: I must be able to check the type requirements (extensively using type traits) in order to disable the assertion compilation and their run-time check.
b) All these solutions leave the assertions in the contracts so the contract code retains its self-documentation value even then the assertion checking is disabled because the type requirements are not met.
c) N1962, Eiffel, D, A++, and all other Contract Programming references that I have seen do not address the issue of the extra type requirements. I am not sure why... Eiffel has generic types but you can always compare them for equality, for non Void, etc.
d) In practice, this might not be a big deal because most of the times old-of is applied to counters (int) and postconditions are the ones introducing the extra requirement but only of EqualityComparable. However, in general I think I need to provide a solution for this issue.

What do you think?

Thanks a lot!
--Lorenzo
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Roman Perepelitsa-3
2011/9/19 lcaminiti <[hidden email]>

>    CONTRACT_FUNCTION_TPL(
>    public void (push_back) ( (const T&) value )
>        precondition(
>            size() < max_size(),
>        )
>        postcondition(
>            auto old_size = CONTRACT_OLDOF size(),
>            auto old_capacity = CONTRACT_OLDOF capacity(),
>            back() == value, // (1)
>            size() == old_size + 1,
>            capacity() >= old_capacity,
>        )
>    ) ;
> };


Why not use SFINAE expressions to disable post conditions that aren't
well-formed? SFINAE expressions feature is required by the C++11 and is
available in several C++03 implementations including gcc and MSVC.

Roman Perepelitsa.

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Stephan T. Lavavej-2
[Roman Perepelitsa]
> SFINAE expressions feature is required by the C++11 and is
> available in several C++03 implementations including gcc and MSVC.

This is incorrect for VC. I've double-checked with our compiler front-end team - expression SFINAE wasn't actively supported in VC10 (and earlier). It sometimes worked by chance. In VC11, due to other bugfixes, it'll work in more cases but still isn't fully supported.

Stephan T. Lavavej
Visual C++ Libraries Developer

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Dave Abrahams
In reply to this post by lcaminiti

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.

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 ;-)

--
Dave Abrahams
BoostPro Computing
http://www.boostpro.com


_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

lcaminiti
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?

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.

Thanks,
--Lorenzo
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Dave Abrahams

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.

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 "==".

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

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

--
Dave Abrahams
BoostPro Computing
http://www.boostpro.com


_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

lcaminiti
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
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

lcaminiti
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 <boost/mpl/bool.hpp>
#include <boost/type_traits/can_call_equal.hpp>
#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
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Vicente Botet
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 <boost/mpl/bool.hpp>
#include <boost/type_traits/can_call_equal.hpp>
#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

Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Jeffrey Lee Hellrung, Jr.-2
In reply to this post by lcaminiti
On Thu, Sep 22, 2011 at 8:03 AM, lcaminiti <[hidden email]> wrote:
[...]

> 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?
>

I'm not sure how you can get away *without* conditionally compiling the
"back() == value" expression, and since your condition is only known at
instantiation time, it seems the only way to effect this is through a
function overload or class specialization.  What is undesirable about the
"extra function call"?

#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==.
>

Agreed.  Again, can you be specific about what the problems with this are?

- Jeff

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

lcaminiti
Jeffrey Lee Hellrung, Jr.-2 wrote
On Thu, Sep 22, 2011 at 8:03 AM, lcaminiti <[hidden email]> wrote:
[...]

> 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?
>

I'm not sure how you can get away *without* conditionally compiling the
"back() == value" expression, and since your condition is only known at
instantiation time, it seems the only way to effect this is through a
function overload or class specialization.  What is undesirable about the
"extra function call"?

#include <boost/mpl/bool.hpp>
> #include <boost/type_traits/can_call_equal.hpp>
> #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==.
>

Agreed.  Again, can you be specific about what the problems with this are?
Yes, the issues are (small):
1) It's harder for me to implement the macros to deal with the extra post1 function definition and call (harder but possible, I think).
2) The run-time overhead of the extra post1 function call-- but if you are really concerned about run-time performances, you'd disable contracts (and especially postconditions) anyway by #defining CONTRACT_CONFIG_NO_POSTCONDITIONS, etc.

So I guess I just roll up my sleeves and implement the macros to expand the extra function calls ;) but I wanted to check with Boosters if there are alternatives to implement this (BTW, I can only use C++03 features to do this).

Thanks a lot!
--Lorenzo
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

lcaminiti
In reply to this post by Vicente Botet
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 <boost/mpl/bool.hpp>
#include <boost/type_traits/can_call_equal.hpp>
#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
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Brent Spillner
In reply to this post by lcaminiti
On Thu, 22 Sep 2011 08:03:09 lcaminiti wrote:
>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?

Unless I'm missing something, you should be able to replace the
post1() calls with

assert(boost::can_call_equal<T>::value && std::clog << "actual
assertion\n" == std::clog && back() == value || std::clog << "trivial
assertion\n" == std::clog);

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Jeffrey Lee Hellrung, Jr.-2
On Thu, Sep 22, 2011 at 10:25 PM, Brent Spillner <[hidden email]> wrote:

> On Thu, 22 Sep 2011 08:03:09 lcaminiti wrote:
> >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?
>
> Unless I'm missing something, you should be able to replace the
> post1() calls with
>
> assert(boost::can_call_equal<T>::value && std::clog << "actual
> assertion\n" == std::clog && back() == value || std::clog << "trivial
> assertion\n" == std::clog);
>

Unfortunately, the compiler can't do a "syntactic short-circuit" when
!can_call_equal<T>::value and simply skip over the "back() == value"
expression; "back() == value" still needs to be a valid expression, i.e., if
an appropriate operator== isn't found, you'll still get a compiler error :(

Compare to

false && (pretty-sure*the==compiler&wont^like%this)

...at least most of the time, anyway...

- Jeff

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Brent Spillner
In reply to this post by Brent Spillner
On Fri, Sep 23, 2011 at 5:25 AM, Brent Spillner <[hidden email]> wrote:
> Unless I'm missing something, you should be able to replace the

Oof, I sure was... that's what I get for posting at 2 in the morning.

I can't see any way around an extra function, but I would probably
encapsulate it with something like

template < class T, class U > typename boost::enable_if_c<
can_call_equal<T>::value, bool >::type
equality_test(const T &t, const U &u) { return t == u; }

bool equality_test(...) { return true; }

to avoid littering the generated class with a bunch of one-off postN()s.

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Brent Spillner
On Thu, 22 Sep 2011 10:30:14 lcaminiti wrote:

>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 fail if L has a private (or protected) operator==.

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

lcaminiti
In reply to this post by Brent Spillner
Brent Spillner wrote
On Fri, Sep 23, 2011 at 5:25 AM, Brent Spillner <[hidden email]> wrote:
> Unless I'm missing something, you should be able to replace the

Oof, I sure was... that's what I get for posting at 2 in the morning.

I can't see any way around an extra function, but I would probably
encapsulate it with something like

template < class T, class U > typename boost::enable_if_c<
can_call_equal<T>::value, bool >::type
equality_test(const T &t, const U &u) { return t == u; }

bool equality_test(...) { return true; }

to avoid littering the generated class with a bunch of one-off postN()s.
Using equality_test works for back() == value. However, in general the assertion can be as complex as you wish so I need to introduce general extra functions postN (littering the user class, my library already litters the user class quite a bit with a number of extra functions, about +5 functions for every member function!! to check pre/postconditions, subcontract, and copy old-ofs). The extra postN functions are only introduced when requires is used on an assertion, so you can chose between generality of the contracts and the cost of the extra functions (to compile and call).

A more complex example:

postcondition(
    auto result = return,
    result == x + y, requires has_equal_to<T>::value && has_plus<T>::value
)

I can't use equality_test here. (This could work with T = int, T = std::string, etc.)

You can construct an arbitrary complex example:

struct airplane {
    bool started ( ) const { ... }
    bool flying () const { ... }
};

struct car {
    bool started ( ) const { ... }
    bool driving () const { ... }
};

postcondition(
    machine.started() && machine.flying(), requires is_airplane<Machine>,
    machine.started() && machine.driving(), requires is_car<Machine>
)

OK this is a silly example, intentionally complex, but it's just to illustrate that equality_test is not generic enough and it won't work in this case.

Thanks.
--Lorenzo
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

lcaminiti
In reply to this post by Brent Spillner
Brent Spillner wrote
On Thu, 22 Sep 2011 10:30:14 lcaminiti wrote:
>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 fail if L has a private (or protected) operator==.
Let me understand your point a bit better. I think you mean something like this:

#include <boost/type_traits/can_call_equal.hpp>
#include <vector>
#include <iostream>
#include <cassert>

namespace dummy {
    template< typename L, typename R >
    bool operator== ( L const& left, R const& right ) {
        std::clog << "dummy ==\n";
        return true;
    }
}

template< typename T >
struct vect {
    void push_back ( T const& value ) {
        v_.push_back(value);
        using dummy::operator==;
        assert( back() == value );
    }

    T const& back ( ) const { return v_.back(); }
private:
    std::vector<T> v_;
};

struct val {
private:
    bool operator== ( val const& right ) const {
        std::clog << "val ==\n";
        return true;
    }
};

int main ( ) {
    vect<val> v;
    v.push_back(val()); // error 1
    std::cout << boost::can_call_equal<val>::value << std::endl; // error 2
    return 0;
};

In this case T = val has an operator== which is private. This causes both the methods (1) using dummy::operator== and (2) the traits requirement can_call_equal<val> to fail :(

Ideally, can_call_equal<val>::value will return false instead of generating a compiler-error when val::operator== is private or protected. A part from such an (impossible?) improvement to can_call_equal, I have no solution for this issue. I can document it and at the end the library users are responsible to program contracts with assertion requirements that can be checked within C++ (and can_call_equal<val> when val has a private operator== cannot be checked so it's simply a ill-formed assertion requirement).

What do you think?

--Lorenzo
Reply | Threaded
Open this post in threaded view
|

Re: [contract] extra type requirements for contracts

Brent Spillner
In reply to this post by lcaminiti
On Fri, 23 Sep 2011 06:45:10 lcaminiti wrote:
>In this case T = val has an operator== which is private. This causes both
>the methods (1) using dummy::operator== and (2) the traits requirement
>can_call_equal<val> to fail :(

Exactly (at least for the default implementation of can_call_equal<>).
 This is in general the behavior you want (can't accidentally apply a
generic operator== to a type with special semantics for which that
wouldn't make sense), but in a contract-checking context I think most
users would rather at least have the option to silently ignore the
untestable constraint.

>Ideally, can_call_equal<val>::value will return false instead of generating
>a compiler-error when val::operator== is private or protected. A part from
>such an (impossible?) improvement to can_call_equal, I have no solution for

Hardly impossible... If you really want the constraint to be tested,
you obviously have to friend the constraint checker class (which may
not always be permissible.)  If you're content to ignore it, just
specialize can_call_equal<perverse_type> to make the nested ::value
false.  Note that some user intervention is still required (adding a
friend to perverse_type, or adding a specialization of
can_call_equal<>), so your contracts won't be silently compiling to
no-ops, but the library user has full control with minimal effort.  As
far as I know, there's no way to offer both options without naming the
test predicate something other than operator==.

Along the same lines, I recognize that test_equality() isn't the only
operation required or supported by the contract mechanism (although
I'll bet it's the most common.)  However, I still believe that a few
test_equality(), test_not_equal(), test_less_than_or_equal(),
operator_add(), etc. stubs, and perhaps a HAS_MEMBER_FUNC() macro to
generate other custom stubs, would enable more readable code than a
postN() method for each constraint.  On the other hand, there is
something to be said for straightforward mechanical generation, and if
you already create 4 other member functions per constraint it's
probably not a big deal.

>What do you think?

Honestly, I think it's a great library, and I hope I can be
disciplined enough to make a habit of using it.

_______________________________________________
Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost
Reply | Threaded
Open this post in threaded view
|

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

lcaminiti
In reply to this post by lcaminiti
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 <boost/type_traits/can_call_equal.hpp>
#include <boost/type_traits/can_call_greater.hpp>
#include <boost/concept_check.hpp>
#include <boost/utility.hpp>
#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