Re: [boost] [contract] assertion requirements as meta-functions or not?

Subject: Re: [boost] [contract] assertion requirements as meta-functions or not?
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-04-24 10:56:39

2012/4/24 lcaminiti <lorcaminiti_at_[hidden]>

>
> Andrzej Krzemienski wrote
> >
> > Hi Lorenzo,
> > If I understand your question and Boost.Contract design correctly, it
> > looks
> > like the former approach is more flexible in cases where I do _not_ want
> > to
> > use a meta-function to describe a constraint:
> >
> >   postcondition(
> >     auto result = return,
> >     some_cond1(result), requires x / 2 == 0,
> >     some_cond2(result), requires noexcept(x),
> >     some_cond3(result), requires sizeof(x) > 2,
> >   )
> >
>
> Yes, that is correct but I was wondering if there's any strong reason in
> favor of using a nullary boolean meta-function instead of sizeof(x) > 2,
> etc
> (I couldn't find such a reason myself and that's why I opted for the static
> boolean value).
>
>
>
> > Although I am not sure if such constraints would be useful in real life.
> >
>
> Assertions requirements are definitely useful for the basic has_equal_to<T>
> case (as you and I discussed a while back). Take the vector<T>::push_back
> example where T is not required to be EqualityComparable by the STL but it
> is if you program the postconditions and that can be modeled as:
>
>    postcondition(
>        back() == value, requires has_equal_to<T>::value
>        ...
>    )
>
> Now you use the contracted vector class as usual and the postcondition is
> checked only when you use such a class on an EqualityComparable type T.
>

Sorry, I guess I was a bit imprecise. I did not want to suggest that
conditional assertions were not useful (I agree with you that they are),
but I was wondering if there is any useful condition that is not a
meta-function. From your examples it looks like there is.

I am not sure if the example where requirements EqualityComparable or
CopyConstructible are stated is the most fortunate one -- someone may argue
that Reularity is so essential tat a special case should be made for it
anyway, similarly to function eq() in:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2012/n3351.pdf. This is
why I like your other example with LessThanComparable better:

https://svn.boost.org/svn/boost/sandbox/contract/libs/contract/doc/html/contract__/examples.html#contract__.examples.__contracts___increment__assertion_requirements_also_for_old_of

Another interesting use of assertion requirements is to model computational
> complexity. Sometimes the contracts can be more expensive to check than the
> body itself :( so it is useful to disable specific assertions that might be
> too expensive (previous N1962 revisions used to do this introducing the
> notion of "importance ordering" then N1962 gave up on this feature --
> assertion requirements are more general than importance ordering and they
> can be used also in this context). For example:
>
> #deifne O_1 0
> #deifne O_N 1
> ...
>
>    postcondition(
>        auto result = return,
>         result == (find(begin(), end(), value) != end()), requires O_N <=
> COMPLEXITY_MAX
>    )
>
> If you compile this code with #define COMPLEXITY_MAX O_N (or greater) than
> this postcondition will be checked otherwise it will neither be compiled
> nor
> checked at run-time.
>
> So using assertion requirements you can program the notion "this assertion
> requires a computational complexity of O(n)" and then enable or disable all
> assertions with a complexity greater than some maximum set complexity
> COMPLEXITY_MAX. IMO, this might be useful too.
>
> (Of course, all this can be done just as well if assertion requirements are
> specified using a nullary boolean meta-functions but I saw no reason for
> that so I'm asking the ML.)
>

This is a nice example. I would also add that there are some assertions
that can be expressed but must never be evaluated because they would alter
the behavior of the function, like iterating over an input range.

Regards,
&rzej