Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrew Sutton (asutton.list_at_[hidden])
Date: 2012-10-01 07:01:10

> This sounds like two questions: "what axioms are for", and "what should
> Boost.Contract do about them".

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. You might also consider using axioms as test cases for
unit testing. 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.

Andrew