Re: [boost] [contract] toward N3351 concepts

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

>
> > I believe that N3351 is not a good place to learn axioms from. I would
> > rather recommend N2887:
> > http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2887.pdf
> > N3351 just did not focus on axioms. Axioms do not necessarily state a
> > boolean predicate. Consider these examples:
> >
> >   *axiom ( Dictionary d, Record r ) {
> >     is_sorted(d) => linear_search(d, r) <=> binary_search(d, r);
> >   }*
> >
> >   * axiom Erasure( Container c, Size n ) {
> >     n == 0 => c.resize(n) <=> c.clear();
> >   }*
> >
> >   * axiom Erasure2( Container c ) {
> >     c.resize(0) <=> c.clear();
> >   }*
> >
> > Especially the last one: it states that two expressions, each with side
> > effects, are equivalent.
>
> I see. Just thinking out loud: If c is a dummy variable, like a local
> variable within the preconditions, then it should be OK if it gets
> modified by the preconditions... shouldn't it?
>

I see (I think) what you are up to, but I see a couple of further issues
with going this way:

(1). Note that in the third example both expressions return nothing (void).
This is valid and desired for axioms. What would you be comparing to check
if the axiom holds?

(2). Axioms need not hold for all values of the given type, but only for
those values that a given algorithm (constrained by a concept with axioms),
and only in expressions that are really stated in the executed algorithm.

For instance, axiom EqualityComparable::Reflexivity states that some
(rather than every) objects must compare equal to themselves. If you
consider type float, objects with value NaN (not-a-number) compare unequal.
Yet, it is still ok to use float as a model of concept EqualityComparable
if the algorithm (function) that makes the use of concept never operates on
NaN-s.

For even more information on axioms see this link:
http://kojot.sggw.waw.pl/~akrzemi1/cpp/axioms/axioms_index.html