Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-09-29 13:01:00

On Wed, Sep 26, 2012 at 12:00 PM, Lorenzo Caminiti
<lorcaminiti_at_[hidden]> wrote:
> 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?

Thanks,
--Lorenzo