Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Evgeny Panasyuk (evgeny.panasyuk_at_[hidden])
Date: 2012-10-05 22:22:25

06.10.2012 5:06, Andrew Sutton wrote:
>> Is it legal "to state" with axioms, something that is not true in
>> general case?
> That's an open question--for me. There may be a good answer to that
> question in the literature or addressed in other domains.

Just to clarify: question was about C++ axioms.
Is it illegal (from formal point of view of C++ axioms), to have:

axiom { a.size() == a.length(); }
and:
int T:size() { return 0;}
int T:length() { return 1;}
?

Does compiler have the authority (from formal point of view of C++ 
axioms) to stop compilation with error in such case(of course, if it 
able to diagnose that)?

> It may be sufficient to simply assume that floating point operations
> satisfy the abstract mathematical requirements. We generally do
> anyways.

For most cases - we may assume floating-point addition associativity. 
For some cases not.
Currently, we may control this by compiler-dependent flags.
For instance /fp:fast /fp:precise flags of MSVC compiler - with /fp:fast 
MSVC2012 does auto-vectorization (SSE) of floating-point accumulation.

If compiler has right to reject wrong axioms when he able to diagnose, 
then we can't use C++ axioms to express in code our assumption about 
floating-point addition associativity.

n3351:
1. "axioms, which express semantics and must not be checked by the 
compiler."
2. "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."

n2887:
3. "Obviously, an implementation may try to check the validity of the 
assumption and give us a suitable error message if it is violated."
4. "As for the “assumptions” that we have had for decades, an 
implementation may (optionally as a quality of implementation issue) 
check some of our uses that can be considered constrained by axiom."

So, I am confused about real intention.

Best Regards,
Evgeny