Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-10-10 12:53:12

On Wed, Oct 10, 2012 at 2:24 AM, Andrzej Krzemienski <akrzemi1_at_[hidden]> wrote:
>>
>> On this topic, I still didn't give up the desire of generating
>> preconditions from axioms and checking them at run-time. N3351 says
>> not to do so because axioms are not constant-correct but given that
>> axioms only alter dummy variables declared within the concepts and not
>> in user code, I don't see why that is a problem (it'd be like allowing
>> preconditions to declare and alter local variables, the state of the
>> user program outside the contract code will still remain unchanged).
>>
>
> Or you could treat axioms more like invariants: check them before and after
> every [I do not know what]. The difference from contracts is that when you
> specify a contract you also implicitly say at which point you expect them
> to be checked. With axioms you just state an "absolute truth" and it is not
> clear how often it should be checked.
>
> Also note this example of axiom that someone here has already brought up:
>
>   axiom Allocation(size_t n)
>   {
>     malloc(n) <=> realloc(0, n);
>   }
>
> If you just create two hidden values p1 and p2:
>
>   auto p1 = malloc(n);
>   auto p2 = realloc(0, n);

The problem here is <=> because I can't implement it (and for example
I can't implement it using p1 and p2 as in the code above). The
problem is not the idea of generating pre, inv, etc for axioms and
checking them at run-time even if they are not const-correct. The
problem is that we write axioms using operations that cannot be
implemented like <=> so we can't actually check axioms.

Is it a good thing to write code that cannot be implemented, compiled,
and executed? IMO, it's not a good thing, that's what code comments
are for. (Again, that's just my opinion and I already said that I see
some value small but > 0 in the syntax checking that we can do with
programming axioms.)

> If you try to compare the values the will be not equal, but the axiom still
> holds.
>
> The major issue I see so far with generating and checking
>> preconditions from axioms is that axioms are programmed using "magic"
>> operations like eq, <=>, is_valid, etc that cannot be implemented :(
>>
>
> I think that to you (the concept library author) only token <=> is the
> magic. Defining function templates eq(),

If <=> is defined as the equivalence operator:

operation1 <=> operation2 ::= "operation1 and operation2 are
equivalent in that they have the same effect on the state of the
program" [1]

Then what you say it's true for eq too. If instead <=> is the logic
if-and-only-if (iff):

predicate1 <=> predicate2 ::= "predicate1 is true if and only if
predicate2 is true" [2]

Then eq() has a special meaning as it is used together with the <=>
iff to state equivalence as defined by [1]. N3351 uses [2] where both
<=> and eq() are magic but I'd prefer [1] where only [1] is magic (and
more powerful). At least that is my understanding.

I will probably implement [1] instead of [2] in my lib. BTW, under [2]
a good alphanumeric name for <=> is "iff". However, what's a good
alphanumeric name for <=> under [1]? (My lib can't use symbols.)

operation1 <=> operation2
(operation1) sameas (operation2) // I like this
(operation1) same_as (operation2)
(operation1) equivals (operation2)

> is_valid() and
> equality_preserving() will be the problem of the users of your library.
> These functions are particular to STL; not to generic programming.

True for all magic operations other than <=> and eq, its users'
defined magic. However, in N3351 equality_preserving and
not_equality_preserving have this magic property that they override
each other from one concept definition to the next... I'm not sure how
users will ever be able to define such operations in a way that they
can implement the overriding property without language or library
support (but then again, these operations are not implementable to
begin with so we don't have to worry about it).

Thanks.
--Lorenzo