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? (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. For even more information on axioms see this link: http://kojot.sggw.waw.pl/~akrzemi1/cpp/axioms/axioms_index.html