A question about DbC

["Jérôme M. Berger"]

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:jeberger at free.fr
http://jeberger.free.fr
Jabber: jeberger at jabber.fr

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <http://lists.puremagic.com/pipermail/digitalmars-d-learn/attachments/20101009/af15c88f/attachment.pgp>