
09.10.2012 3:03, Lorenzo Caminiti wrote:
name should be chosen. Axioms are: 1) Formal and clear language to talk about semantics. I disagree, I think it'd be great if compilers could check the semantics of programs (I know it's impossible, but it'd be great). So given that axioms state the semantics of concepts and that I'd like to
I hope C++ Axioms are not about any kind of checking, otherwise some other the compiler to check the semantics of programs, I'd like the compiler to check the axioms (but again, unfortunately I understand that it cannot be done).
Besides of fact that it can't be checked in general way, just imagine that it could: What about types which fulfil axioms only on some set of values, and only in some cases? How "checker" would distinguish cases when it is OK to have types which fulfil axioms partly, and when it is not? Let's get back to NaN's: concept TotallyOrdered<EqualityComparable T> = requires (T a, T b, T c) { ... axiom { ... a < b || b < a || a == b; } ... }; ____ #include <iostream> #include <limits> #include <cassert> using namespace std; int main() { double a=numeric_limits<double>::quiet_NaN(); double b=numeric_limits<double>::quiet_NaN(); cout << (a < b); cout << (b < a); cout << (a == b); assert( (a < b) || (b < a) || (a == b) ); return 0; } http://ideone.com/Q8l17 stdout : 000 stderr : prog: prog.cpp:13: int main(): Assertion `(a < b) || (b < a) || (a == b)' failed. ____ OK, compiler would prove that double type does not fulfil TotallyOrdered concept's axiom. And now, it will reject following algorithm when used on array of doubles: template<ForwardIterator I, TotallyOrdered T, Relation<ValueType<I>, T> R> I lower_bound(I first, I last, const T& value, R comp); Do you agree to forbid usage of lower_bound on array of doubles? Or what mechanism should be used to allow types which fulfil axioms only partly? axiom_cast<double,TotallyOrdered> ? Best Regards, Evgeny