A question about DbC

[bearophile]

J. Berger:

> 	Jonathan's point is not about running the post-condition and the
> invariant. It is about running the invariant twice: both before and
> after the function. This is completely independent from any pre- or
> post-conditions there may be.

You are missing something still.

C = a class with Dbc
foo = nonstatic method of C
fooargs = input arguments of foo
r = result of foo
S = state of the class instance foo
fooS = a subset of S, the part of the state influenced by foo
noFoo = S - fooS = part of S not influenced by foo
Inv = C invariant, that tests for coherence of the whole S
prefoo = pre-condition of foo
postfoo = post-condition of foo

Let's say DMD runs things in this order (this is not currently true but I think this is more correct):
Inv prefoo foo postfoo Inv

Then:
- The first Inv tests that S is coherent
- prefoo tests that fooargs are correct (and maybe even that fooS is correct)
- postfoo tests that r and fooS are correct
- Inv tests that S is coherent

It's necessary to run Inv before and after foo because postfoo has not tested that the whole S is coherent.

foo is able to modify just fooS, it can't touch noFoo, but you need to run Inv again because inside Inv it may be present a predicate1(fooS, noFoo) that is true according to the relation between fooS and noFoo. So even if noFoo is unchanged, changes to fooS may be enough to invalidate predicate1.

Bye,
bearophile