On Mon, Oct 1, 2012 at 4:01 AM, Andrew Sutton <asutton.list@gmail.com> wrote:
This sounds like two questions: "what axioms are for", and "what should Boost.Contract do about them".
This is fair. However, we could also say: (1) what axioms are for, (2) what should C++1x do about them, and (3) Boost.Contract should do with axioms as close as possible as C++1x does with axioms.
I think that sums up the problem quite well.
I think there is some merit in putting axioms into concepts. ... snip
Third, compilers could make use of the declarations in axioms (even if they cannot validate the "correctness" of an axiom). This is more-less how copy elision works. It works under unverifiable assumption that copy constructor does nothing else but creating a copy of the original object and the destructor does nothing else but destroying an object. This assumption does not always hold: for instance you may be doing some logging in the constructor (and be surprised that the logging vanishes), but compilers are nonetheless allowed to do such substitution (which is in fact an elimination of constructor and destructor call). If we had axioms we could specify copy elision as an axiom, say:
* axiom CopyElision( T v ) {* * { T(v); } <=> {} * * }*
And need not define any special rules for copy elision in the standard. (Well, I know it would not work, but you get the idea.)
I think that trying to define the semantics of the language from within the language gets us to shaky ground because we can't say under what circumstances a copy could be elided.
But again, we're in an early state of design w.r.t. a proposal for how axioms might actually be used, and I'm not particularly knowledgeable of those details. I can only say with confidence that it's being worked on.
Regarding question "what should Boost.Contract do about axioms", my opinion is that you should only check them against C++ syntax and type safety. That is, if you see this axiom:
*concept BidirectionalIterator<ForwardIterator I> = requires decrement (I i, I j) { axiom { is_valid(––i) <=> is_valid(i––); is_valid(i––) => (i == j => i–– == j); is_valid(i––) => (i == j => (i––, i) == ––j); } ...*
You should check if expressions: *is_valid(––i), **is_valid(i––)*, *i == j*, *i–– == j*, *(i––, i) == ––j *are valid (compilable), and that's it. That is, whoever is defining concept *BidirectionalIterator *must make sure that function *is_valid *is in scope and does something -- not you.
Yes, and you'll never be able to actually do anything programmatically with is_valid.
Same for eq(), <=>, and =>, I can't do anything programmatically with them neither, can I? Just to clarify, when I say to use code comments, you could use programming-style comments. So the difference is between: concept BidirectionalIterator<ForwardIterator I> = // (a) requires decrement (I i, I j) { axiom { is_valid(––i) <=> is_valid(i––); is_valid(i––) => (i == j => i–– == j); is_valid(i––) => (i == j => (i––, i) == ––j); } ... And: concept BidirectionalIterator<ForwardIterator I> = // (b) requires decrement (I i, I j) { // axiom { // is_valid(––i) <=> is_valid(i––); // is_valid(i––) => (i == j => i–– == j); // is_valid(i––) => (i == j => (i––, i) == ––j); // } ... As Andrzej pointed out, (a) is better than (b) because the compiler will error if the axioms get out of sync with the rest of the concept (change type/variable name I, i, j, etc). Any other reason to favor (a) over (b)? (Leaving a side possible future compiler optimizations that might never come and that will not be possible with a lib like Boost.Contract in any case.) IMO, with (b) is more clear that axioms don't actually check anything while (a) can be misleading causing programmers to think that the expressed semantics of the concept will actually be checked and enforced by the program. I guess it's only fair to assume that programmers read the docs and understand that axioms _document_ but don't actually check or enforce the semantics. At the end, I'm thinking that there's value in the syntax checking provided by (a) over (b) (even if I wish (a) could check and enforce more of the semantics maybe generating preconditions to check at run-time for the concept... I'm not sure...).
You might also consider using axioms as test cases for unit testing.
BTW, this is true for pre/post conditions as well.
This is something that was done by a group in Bergen using a metacompiler.
http://www.jot.fm/issues/issue_2011_01/article10.pdf
The paper should be free. If not, I can email a version (off-list, of course) to anybody that is interested.
And I just returned from presenting a paper on testing generic libraries where I discussed a manual approach to the same problem. The paper hasn't been published yet, but I can make a copy available if you are interested.
Thanks, --Lorenzo