I guess I have to put it together myself in order to make it easier to follow. Apparently the problem was this:
Consider the following program segment:
Code:
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 [MATH]x=y[/MATH], then which condition is its precondition?
a) [MATH]x=2y[/MATH] and [MATH]y<2[/MATH]b) [MATH]x>2y[/MATH] and [MATH]y=2[/MATH]c) [MATH]x=2y[/MATH] and [MATH]y>2[/MATH]d) [MATH]x<2y[/MATH] and [MATH]y>2[/MATH]
Since you only said those were
some of the choices, I'm not sure. Is this exactly what it said?
If this is asking which of the listed conditions must be true initially in order for the program to terminate, then I think the problem is bad. I seem to have proved that it will terminate whenever x is a non-negative integer.
You could try running the program with sets of inputs corresponding to the negation of the various choices and see whether it fails to terminate. For example, if I take x=4 and y=2, I have not satisfied (a) or (c), but it does terminate, so (a) and (c) can't be right. I believe you can similarly eliminate the other choices.
All that leaves, in my mind, besides a simply bad (or miscopied) problem, is that your definition of precondition may not be what I think it is. Can you quote the definition you were given? (I would have agreed with posts #3, 4, 7.)