Re: [Ass3] If pre-post and while

From: Anja Karl <anja.karl ***AT***>
Date: Fri, 25 Nov 2016 20:00:52 +0100
Subject: Re: [Ass3] If pre-post and while
Organization: Technische Universitaet Graz
Message-id: <o1a1bo$2od$>
User-agent: Postbox 4.0.8 (Windows/20151105)
References: <o193r2$hm8$>

1) it is for if without else... there you have to check, that pre and post fit, if the if body is not executed.

2) Yes, you are right, the loop post body is an old relict and can be ignored.


Matthias Eder schrieb:

i am implementing the If condition and I am wondering what the "if
pre-post" type has to check? The precondition of the if is {P} and the
postcondition is {Q}, so you cannot compare them directly or did I
forget something?

And why do we have 4 types for the loop condition? I do not know when to
use the "loop post body" condition? Also the example output for
search.wrong doesn't show this output?

Cheers Matthias