Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrew Sutton (asutton.list_at_[hidden])
Date: 2012-09-28 05:39:02

>> 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)
>
> Wouldn't this mean the following? For any p and q of some type T:
>
> p = malloc(n);
> q = realloc(0, n);
> assert( eq(p, q) );
>
> Where eq() is the N3351 equality operator that checks if two objects
> are equal. eq could be implemented using == but it's more of a logical
> equality so even if a type doesn't have == than it is still logically
> sensible to check if two objects for that type are the same. In
> reality however, eq will have to be implemented and checkable somehow
> so if a type doesn't have a way to programatically checked for
> equality (using == or some other boolean function eq(), equal(),
> is_equal(), etc) then either you don't program the axiom or you add an
> assertion requirement to guard against the lack of == (like
> Boost.Contract does):

*cringe* Don't think about eq(). That was a compromise between myself
and Marcin Zalewski. We couldn't determine if <=> should be
interpreted as logical equivalence or behavioral equivalence (as in
the previous axioms work). We ended assigning <=> to logical
equivalence and using eq() as a kind of oracle that decided equality:
either according to the rules of == or memberwise equality comparison.

In retrospect, I think this was the wrong choice. Using <=> to
describe the behavioral equivalence of two expressions provides a much
more robust way of stating the relative meaning of operations.

Andrew