Boost logo

Boost :

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


Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk