On Wed, Oct 10, 2012 at 2:24 AM, Andrzej Krzemienski <akrzemi1@gmail.com> 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