Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-10-11 14:54:44

On Thu, Oct 11, 2012 at 12:46 AM, Andrzej Krzemienski
<akrzemi1_at_[hidden]> wrote:
> 2012/10/10 Evgeny Panasyuk <evgeny.panasyuk_at_[hidden]>
>
>> 10.10.2012 11:57, Andrzej Krzemienski wrote:
>>
>>> P.S. I just have wild idea - what about axioms for function's arguments?
>>>> i.e. not on types, but on values.
>>>> Maybe some kind of axiomatic_assert.
>>>> For instance that can be used to prevent pointers aliasing ("restrict"
>>>> keyword in C99):
>>>> void* memcpy( void* dest, const void* src, size_t count )
>>>> {
>>>>      axiomatic_assert( do_not_overlap(dest,src,count) );
>>>>      // ...
>>>> }
>>>>
>>>>  Is this not the same thing as preconditions in contract programming and
>>> Lorenzo's Boost.Contract library?
>>>
>>>
>> 1. I have just looked to http://www.open-std.org/jtc1/**
>> sc22/wg21/docs/papers/2006/**n1962.html<http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html>referenced in Boost.Contract.
>> I assumed that it was not about performance, but only about runtime
>> checking. So, I am little bit surprised that it considers performance also.
>>
>> Anyway, I supposed that axiomatic_assert MUST never check it's assertions
>> - it is just pure language to talk with optimizer. And as for concept's
>> axioms, I think user legally (from the formal point of view) can make
>> axiomatic_assert on properties which are not true in general case - so this
>> is main difference.
>>
>> There are cases, when checking of pre-conditions would make impossible to
>> achieve function's post-conditions (I think already mentioned here), for
>> instance:
>> a) multi-passing sequence represented by Input Iterator.
>> b) lower_bound: if check that it's input range is sorted, then
>> post-condition regarding number of logarithmic comparisons will be broken.
>> Maybe this is OK in unit-tests, but I don't think it is OK even in Debug
>> builds.
>>
>> 2. I don't think that Lorenzo's Boost.Contract library able to enable any
>> optimizations, at least while we don't have some kind of support from
>> compiler.
>> While main purpose of axiomatic_assert(which I think of) is
>> optimizability, like preventing pointers aliasing and so on.
>
>
> Ok, I think I now know what you are saying: axiomatic_assert states what
> compilers are allowed to assume, but what they are not allowed to check.
> This does differ from the typical usage of preconditions; but I still
> believe that preconditions in contract-programming sense should be able to
> offer this capability already. I am talking about contract-programming as
> language feature, because library-based solutions offer little help to the
> optimizer.
>
> Lorenzo's library offers the capability of declaring preconditions that
> must never be executed. This addresses your examples above (with
> InputIterator-based range and runtime complexity of lower_bound). See here:
> http://contractpp.svn.sourceforge.net/viewvc/contractpp/releases/contractpp_0_4_1/doc/html/contract__/advanced_topics.html#contract__.advanced_topics.assertion_requirements
>
> In short, you can express an assertion and attach a condition when (if
> ever) it should be checked. In ideal syntax, it would be written as:
>
>   template <class It>
>   requires InputIterator<It>
>   size_t distance(It b, It e)
>   precondition(is_range(b, e), MultiPassIterator<It>)
>   {
>   }

A small note (not really relevant for this discussion) is that I
recently find out that the ideal syntax to express assertion
requirements is to use "static if" as proposed by N3329:

template< typename I >
    requires InputIterator<I>
size_t distance ( I b, I e )
    precondition {
        static if(MultiPassIterator<I>) { is_range(b, e); }
    }
{
    ... // implementation
}

Boost.Contract will adopt such a syntax on its 1st release:
http://sourceforge.net/apps/trac/contractpp/ticket/101

> The second argument in precondition (MultiPassIterator<It>) says under what
> (static) condition the compiler is allowed to perform the check. If you
> want to disable the check forever (but still want to express that this is
> an assumption that compilers can make),
>
>   precondition(is_range(b, e), false)

precondition {
    static if(false) is_range(b, e);
}

> To wrap up, I believe that contract-programming's primary feature is to be
> able to express assumptions that you may hold for granted. Being able to
> check these at run-time is just a bonus.

--Lorenzo