bearophile wrote:
> 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.
>
No.
> ... example pseudo-code
This is more or less what Jonathan said in his last post.
Jerome
--
mailto:jeber...@free.fr
http://jeberger.free.fr
Jabber: jeber...@jabber.fr
signature.asc
Description: OpenPGP digital signature
