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

Originally on math.SE but unanswered there.

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.

Gilles is right that the general technique is to go fishing for interesting observations.

In this case, you may observe that the program is an instance of binary search, because it has the following shape:

while i + 1 != k
  j := strictly_between(i, k)
  if f(j)  X then k := j

Then you just plug in your particular f, X, ... into the general invariant for binary search. Dijkstra has a nice discussion of binary search.

StackExchange Computer Science Q#288, answer score: 9