On Wed, Sep 26, 2012 at 2:56 PM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
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.
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? --Lorenzo