# Boost :

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:

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