A question about DbC

"Jérôme M. Berger" jeberger at free.fr
Sat Oct 9 07:08:53 PDT 2010

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.

mailto:jeberger at 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>

More information about the Digitalmars-d-learn mailing list