Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-10-11 03:46:57

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>)
  {
  }

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)

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.

Regards,
&rzej