Boost logo

Boost :

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(); }
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.

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

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,

Boost list run by bdawes at, gregod at, cpdaniel at, john at