On Thu, Sep 27, 2012 at 3:35 AM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
I believe that N3351 is not a good place to learn axioms from. I would rather recommend N2887: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2887.pdf N3351 just did not focus on axioms. Axioms do not necessarily state a boolean predicate. Consider these examples:
*axiom ( Dictionary d, Record r ) { is_sorted(d) => linear_search(d, r) <=> binary_search(d, r); }*
* axiom Erasure( Container c, Size n ) { n == 0 => c.resize(n) <=> c.clear(); }*
* axiom Erasure2( Container c ) { c.resize(0) <=> c.clear(); }*
Especially the last one: it states that two expressions, each with side effects, are equivalent.
I see. Just thinking out loud: If c is a dummy variable, like a local variable within the preconditions, then it should be OK if it gets modified by the preconditions... shouldn't it?
I see (I think) what you are up to, but I see a couple of further issues with going this way:
(1). Note that in the third example both expressions return nothing (void). This is valid and desired for axioms. What would you be comparing to check if the axiom holds?
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.
(2). Axioms need not hold for all values of the given type, but only for those values that a given algorithm (constrained by a concept with axioms), and only in expressions that are really stated in the executed algorithm.
For instance, axiom EqualityComparable::Reflexivity states that some (rather than every) objects must compare equal to themselves. If you consider type float, objects with value NaN (not-a-number) compare unequal. Yet, it is still ok to use float as a model of concept EqualityComparable if the algorithm (function) that makes the use of concept never operates on NaN-s.
Yes, I'm reading about this... N3351 says that preconditions can limit the values to well formed values (that makes sense) so maybe combing preconditions with concepts and check the axioms only for the values that pass the preconditions... again, just thinking out loud while still readingN3351.
For even more information on axioms see this link: http://kojot.sggw.waw.pl/~akrzemi1/cpp/axioms/axioms_index.html
Thanks! --Lorenzo