Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-09-27 13:11:30

On Thu, Sep 27, 2012 at 3:35 AM, Andrzej Krzemienski <akrzemi1_at_[hidden]> wrote:
>>
>> > 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?
>>
>
> I see (I think) what you are up to, but I see a couple of further issues
> with going this way:
>
> (1). Note that in the third example both expressions return nothing (void).
> This is valid and desired for axioms. What would you be comparing to check
> if the axiom holds?

Again, I'm learning these things as we go... but aren't => and <=> the
"implies" and "if and only if" logical operators? If so, their operand
must be boolean predicates so I don't understand what this axioms
means:

c.resize(0) <=> c.clear()

Oh, I see, <=> is some sort of magic "equivalence" operator as it can
be defined only meta+programmatically in the programmer's mind. This
axiom means that "the effect of c.resize(0) must be /equivalent/ to
c.clear()" in a way that the program will never be able to assert. I
can't even check that syntactically, can I? What does it mean to check
the axiom above syntactically given that I'd have to completely strip
away the <=> operator because it cannot be represented
programmatically? Then such an axiom is just a code comment and maybe
it should be programmed as such IMO.

> (2). Axioms need not hold for all values of the given type, but only for
> those values that a given algorithm (constrained by a concept with axioms),
> and only in expressions that are really stated in the executed algorithm.
>
> For instance, axiom EqualityComparable::Reflexivity states that some
> (rather than every) objects must compare equal to themselves. If you
> consider type float, objects with value NaN (not-a-number) compare unequal.
> Yet, it is still ok to use float as a model of concept EqualityComparable
> if the algorithm (function) that makes the use of concept never operates on
> NaN-s.

Yes, I'm reading about this... N3351 says that preconditions can limit
the values to well formed values (that makes sense) so maybe combing
preconditions with concepts and check the axioms only for the values
that pass the preconditions... again, just thinking out loud while
still readingN3351.

> For even more information on axioms see this link:
> http://kojot.sggw.waw.pl/~akrzemi1/cpp/axioms/axioms_index.html

Thanks!
--Lorenzo