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
