Precondition of while loop program?

218 Views Asked by At

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!