A question about DbC

[bearophile]

Jonathan M Davis:

> if the state couldn't have changed since the last public function call, the running
> the invariant before the function call is pointless.

The post-condition of a method doesn't need to make sure the class is in a correct state, all it has to test is that its output (including the instance state it has modified) is correct.

The invariant instead has to test that the whole class instance is in a meaningful state. So method post-condition and class invariant contain different code and they must be run both, because the post-condition has to test just the class instance state it has changed, and not that such changes are globally coherent with the whole class instance state.

Bye,
bearophile