Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-09-26 17:56:22

>
> For now, I find this argument for not generating preconditions from
> axioms weak. How about you can only use constant expressions within
> axioms because axioms (as contracts and specifically preconditions)
> are not supposed to alter the program's stats? Then I can
> automatically generate preconditions from axioms and check them at
> run-time--why would this be a bad idea? Then you need to implement a
> constant-correct version of distance() in order to program the axiom
> but that's a good thing IMO... (it reflects the fact that axioms
> should not alter the program's state).
>

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.