However, N3351 says that axioms should not be checked by the compiler...
``Axioms express the semantics of a concept’s required syntax; they are assumed to be true and must not be checked by the compiler beyond conformance to the C++ syntax. Any additional checking is beyond the scope of the compiler’s translation requirements. The compiler must not generate code that evaluates axioms as preconditions, either. This could lead to program errors if the evaluated assertions have side effects. For example, asserting that distance(first, last) > 1 when the type of those iterators is istream_iterator will consume the first element of the range, causing the assertion to pass, but the algorithm to have undefined behavior.''
So what am I supposed to do with axioms? Do nothing? Axioms are just "comments" that document the semantic?
All: I'm still struggling with my original question... what am I supposed to programatically do with axioms?
Take a look at this axioms--is_valid is not implementable... what would I check here?
concept BidirectionalIterator<ForwardIterator I> = ... requires decrement (I i, I j) { ... axiom { is_valid(––i) <=> is_valid(i––); is_valid(i––) => (i == j => i–– == j); is_valid(i––) => (i == j => (i––, i) == ––j); }
Same thing for the magic eq() that is not implementable (if not trivially as operator==). And if we get rid of eq and define <=> as equivalence instead of iff then <=> is not implementable. Even just checking axiom's syntax... what does that mean if I cannot implement eq, is_valid, <=>, etc? I don't understand...
It seems to me that we are writing axioms using a bunch of non-implementable operations... IMO, if axioms cannot be checked programatically, either syntactically at compile-time and/or with run-time assertions, then they should just be noted as code comments... Why would I program (axiom) code that is neither compiled nor executed?
This sounds like two questions: "what axioms are for", and "what should Boost.Contract do about them". Regarding the first, your concerns are about the same as the members of the Committee had when the concepts were being standardised (see here: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2848.html). Some observed even more concerning thing: compilers would be allowed to replace one expression with another, but there would be no way to check if the two expressions are equivalent. I think there is some merit in putting axioms into concepts. First, there are for you: the programmer, not to compiler. When you see that function fun<T> requires that T is a StrictWeekOrdering, you want to know what the concept expects of your type, you want to read it, and axiom tells you that. You could type in the comment "it must be transitive" but this is too informal. Second, rather than a normal comment, they are a syntax-checked comment: if you rename your variables or type names in concept definition, the compiler will remind you that you also need to change the axiom. It is somewhat similar to asserts. Even if you disable them both in production and debug code, they are still useful: because you can reed what they state, and if what they state is grammatically correct (see http://akrzemi1.wordpress.com/2011/04/06/assertions/). Third, compilers could make use of the declarations in axioms (even if they cannot validate the "correctness" of an axiom). This is more-less how copy elision works. It works under unverifiable assumption that copy constructor does nothing else but creating a copy of the original object and the destructor does nothing else but destroying an object. This assumption does not always hold: for instance you may be doing some logging in the constructor (and be surprised that the logging vanishes), but compilers are nonetheless allowed to do such substitution (which is in fact an elimination of constructor and destructor call). If we had axioms we could specify copy elision as an axiom, say: * axiom CopyElision( T v ) {* * { T(v); } <=> {} * * }* And need not define any special rules for copy elision in the standard. (Well, I know it would not work, but you get the idea.) Regarding question "what should Boost.Contract do about axioms", my opinion is that you should only check them against C++ syntax and type safety. That is, if you see this axiom: *concept BidirectionalIterator<ForwardIterator I> = requires decrement (I i, I j) { axiom { is_valid(––i) <=> is_valid(i––); is_valid(i––) => (i == j => i–– == j); is_valid(i––) => (i == j => (i––, i) == ––j); } ...* You should check if expressions: *is_valid(––i), **is_valid(i––)*, *i == j*, *i–– == j*, *(i––, i) == ––j *are valid (compilable), and that's it. That is, whoever is defining concept *BidirectionalIterator *must make sure that function *is_valid *is in scope and does something -- not you. Regards, &rzej