Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Evgeny Panasyuk (evgeny.panasyuk_at_[hidden])
Date: 2012-10-10 14:10:43

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

Best Regards,
Evgeny