Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-09-30 14:32:35

>
> > However, N3351 says that axioms should not be checked by the compiler...
> >
> > ``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. Any additional
> > checking is beyond the scope of the compiler’s translation
> > requirements. The compiler must not
> > generate code that evaluates axioms as preconditions, either. This
> > could lead to program errors
> > if the evaluated assertions have side effects. For example, asserting
> > that distance(first, last) > 1
> > when the type of those iterators is istream_iterator will consume the
> > first element of the range,
> > causing the assertion to pass, but the algorithm to have undefined
> behavior.''
> >
> > So what am I supposed to do with axioms? Do nothing? Axioms are just
> > "comments" that document the semantic?
>
> All: I'm still struggling with my original question... what am I
> supposed to programatically do with axioms?
>
> Take a look at this axioms--is_valid is not implementable... what
> would I check here?
>
> 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);
>         }
>
> Same thing for the magic eq() that is not implementable (if not
> trivially as operator==). And if we get rid of eq and define <=> as
> equivalence instead of iff then <=> is not implementable. Even just
> checking axiom's syntax... what does that mean if I cannot implement
> eq, is_valid, <=>, etc? I don't understand...
>
> It seems to me that we are writing axioms using a bunch of
> non-implementable operations... IMO, if axioms cannot be checked
> programatically, either syntactically at compile-time and/or with
> run-time assertions, then they should just be noted as code
> comments... Why would I program (axiom) code that is neither compiled
> nor executed?
>

This sounds like two questions: "what axioms are for", and "what should
Boost.Contract do about them". Regarding the first, your concerns are about
the same as the members of the Committee had when the concepts were being
standardised (see here:
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2848.html). Some
observed even more concerning thing: compilers would be allowed to replace
one expression with another, but there would be no way to check if the two
expressions are equivalent.

I think there is some merit in putting axioms into concepts. First, there
are for you: the programmer, not to compiler. When you see that function
fun<T> requires that T is a StrictWeekOrdering, you want to know what the
concept expects of your type, you want to read it, and axiom tells you
that. You could type in the comment "it must be transitive" but this is too
informal. Second, rather than a normal comment, they are a syntax-checked
comment: if you rename your variables or type names in concept definition,
the compiler will remind you that you also need to change the axiom. It is
somewhat similar to asserts. Even if you disable them both in production
and debug code, they are still useful: because you can reed what they
state, and if what they state is grammatically correct (see
http://akrzemi1.wordpress.com/2011/04/06/assertions/). 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.)

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.

Regards,
&rzej