Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-09-26 18:38:34

On Wed, Sep 26, 2012 at 2:56 PM, Andrzej Krzemienski <akrzemi1_at_[hidden]> wrote:
>>
>> For now, I find this argument for not generating preconditions from
>> axioms weak. How about you can only use constant expressions within
>> axioms because axioms (as contracts and specifically preconditions)
>> are not supposed to alter the program's stats? Then I can
>> automatically generate preconditions from axioms and check them at
>> run-time--why would this be a bad idea? Then you need to implement a
>> constant-correct version of distance() in order to program the axiom
>> but that's a good thing IMO... (it reflects the fact that axioms
>> should not alter the program's state).
>>
>
> I believe that N3351 is not a good place to learn axioms from. I would
> rather recommend N2887:
> http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2887.pdf
> N3351 just did not focus on axioms. Axioms do not necessarily state a
> boolean predicate. Consider these examples:
>
>   *axiom ( Dictionary d, Record r ) {
>     is_sorted(d) => linear_search(d, r) <=> binary_search(d, r);
>   }*
>
>   * axiom Erasure( Container c, Size n ) {
>     n == 0 => c.resize(n) <=> c.clear();
>   }*
>
>   * axiom Erasure2( Container c ) {
>     c.resize(0) <=> c.clear();
>   }*
>
> Especially the last one: it states that two expressions, each with side
> effects, are equivalent.

I see. Just thinking out loud: If c is a dummy variable, like a local
variable within the preconditions, then it should be OK if it gets
modified by the preconditions... shouldn't it?

--Lorenzo