# How is the loop invarient obtained in this square root bound finding algorithm?

Consider the following algorithm.

u := 0
v := n+1;
while ( (u + 1) is not equal to v) do
x :=  (u + v) / 2;
if ( x * x <= n)
u := x;
else
v := x;
end_if
end_while


where u, v, and n are integers and the division operation is integer division.

• Explain what is computed by the algorithm.
• Using your answer to part I as the post-condition for the algorithm, establish a loop invariant and show that the algorithm terminates and is correct.

In class, the post-condition was found to be $0 \leq u^2 \leq n < (u + 1)^2$ and the Invariant is $0 \leq u^2 \leq n < v^2, u + 1 \leq v$. I don't really understand on how the post-condition and invariants were obtained. I figure the post condition was $u + 1 = v$... which is clearly not the case. So I am wondering on how the post-condition and invariant was obtained. I'm also wondering on how the pre-condition can be obtained by using the post-condition. Thanks for the help.

-
Is your problem understanding why the algorithm works, or just with converting this understanding into a loop-invariant style correctness proof? (Note that finding appropriate invariants is not a mechanical process; it depends crucially on understanding how the program is supposed to work). –  Henning Makholm Oct 21 '11 at 2:12
This question has been reposted and answered on Computer Science: How is the loop invariant obtained in this square root bound finding algorithm? –  Gilles Jul 8 '12 at 1:08