Boost logo

Boost :

Subject: Re: [boost] [contract] toward N3351 concepts
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-09-26 18:38:34

On Wed, Sep 26, 2012 at 2:56 PM, Andrzej Krzemienski <akrzemi1_at_[hidden]> 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:
> 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?


Boost list run by bdawes at, gregod at, cpdaniel at, john at