Question

Consider the following program (written in pseudo-code)

begin
x:= 0;
y:= 1;
z:= 1;
while y <= n do
x:= x+1;
z:= z+2;
y:= y+z;
od
sqrt := x;
end

Prove the partial correctness of the program with respect to the following predicates:

Pre: {n>=0}

Post: {sqrt2 <= n and n < (sqrt+1)2
)

That is,
{Pre}
begin
x:= 0;
y:= 1;
z:= 1;
while y <= n do
x:= x+1;
z:= z+2;
y:= y+z;
od
sqrt := x;
end
{Post}