Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-09-27 15:10:45

On Thu, Sep 27, 2012 at 12:03 PM, Nathan Ridge <zeratul976_at_[hidden]> wrote:
>
>> 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.
>
> Perhaps we can interpret this formally as "all the variables that appear
> in both expressions [in this case, c] compare equal after the expressions
> are evalauted"?

Yeah, I was thinking more about it and maybe we can program it more or
less like this:

c1.resize(0);
c2.clear();
assert( eq(c1, c2) ); // the actual check

For every (this "for every" part is going to be hard to implement) c1
and c2 of type C and where eq returns true iff c1 and c2 are equal (eq
could be implemented as operator== at least to start with).

--Lorenzo