Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-10-01 14:55:57

On Mon, Oct 1, 2012 at 4:01 AM, Andrew Sutton <asutton.list_at_[hidden]> 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