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

22 Sep 2011

      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

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