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