Precondition of while loop program?

$\begingroup$

I am having trouble finding precondition for the following program. Consider the following program segment:

x:=x+y;
if (x<0) then abort
else while (x != y) do x:=x+1; y:=y+2 od
fi

If it is assumed that its postcondition is ${x = y}$, then which condition is its precondition?

These are some of the choices that professors at my university make:

a) $x=2y$ and $y < 2$

b) $x>2y$ and $y=2$

c) $x=2y$ and $y>2 $

d) $x<2y$ and $y>2$

Hope for the help of everyone. Thanks for very much!

$\endgroup$ 6 Sorted by: Reset to default

Know someone who can answer? Share a link to this question via email, Twitter, or Facebook.