bearophile wrote:
> 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.
>
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.
Jerome
--
mailto:jeber...@free.fr
http://jeberger.free.fr
Jabber: jeber...@jabber.fr
signature.asc
Description: OpenPGP digital signature
