Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Marc Glisse (marc.glisse_at_[hidden])
Date: 2012-09-27 15:29:35

On Thu, 27 Sep 2012, Lorenzo Caminiti wrote:

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

One could write axioms for types that don't have an operator==, or where 
comparison doesn't make sense:
p=malloc(n) <=> p=realloc(0,n)
v.random_shuffle().random_shuffle() <=> v.random_shuffle()
(x+y)+z <=> x+(y+z) for double (somewhat like passing -fassociative-math
   to gcc)

-- 
Marc Glisse