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!