Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Evgeny Panasyuk (evgeny.panasyuk_at_[hidden])
Date: 2012-10-08 20:02:58

09.10.2012 3:03, Lorenzo Caminiti wrote:
>> I hope C++ Axioms are not about any kind of checking, otherwise some other
>> >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
> 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