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.

• Are you familiar with Hoare logic, and do you expect an answer to touch it? – Raphael Mar 13 '12 at 7:32

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 i := j
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.

$u+1=v$ is indeed a post-condition of the while loop (why do you think it's “clearly” not the case?). This is always the case with a while loop that doesn't contain a break: when the loop exits, it can only be because the loop condition (here, $u+1 \neq v$) is false. It's not the only thing that will be true when the loop exits here (this algorithm actually computes something interesting, as you saw in your class, so $u = \text{[this interesting thing]}$ and $v = \text{[this interesting thing]}$ are also post-conditions), but it is the most obvious.

Now, to find other interesting properties, there's no general recipe. In fact, there is some formal sense in which there is no general recipe to find loop invariants. The best you can do is apply some techniques that only work in some cases, or generally go fishing for interesting observations (which works better and better as you get more experienced).

If you run the loop for a few iterations with some value of $n$, you'll see that at each iteration:

• either $u$ jumps up to $(u+v)/2$;
• or $v$ jumps down to $(u+v)/2$.

In particular, $u$ starts less than $v$, and will never overtake it. Furthermore, $u$ starts positive and increases, while $v$ starts at $n+1$ and decreases. So $0 \le u \le v \le n+1$ is an invariant throughout this program.

One thing that's not so obvious is whether $u$ can ever be equal to $v$. That's important: if $u$ and $v$ ever become equal, we'll have $x = u = v$ and the loop will keep going forever. So you need to prove that $u$ and $v$ never become equal in order to prove that the algorithm is correct (i.e. does not loop forever). Once this need has been identified, it is easy to prove (I'm leaving this as an exercise) that $u < v$ is a loop invariant (keep in mind that $u$ and $v$ are integers, so this is equivalent to $u+1 \le v$).

Since $v = u+1$ at the end of the program, the post-condition you were given can also be written $u^2 \le n < v^2$ (the part $0 \le u^2$ is trivial). The reason we want a post-condition like this, involving $n$, is that we want to tie the result of the program with the input $n$. Why this precise condition? We're looking for something that's as precise as possible, and we look at where $n$ appears inside the loop:

• we have $u \le x \le v$;
• when $x^2 \le n$, we pick the next $u$ to be $x$, so that $u^2 \le n$ (and $v$ doesn't change);
• when $x^2 > n$, we pick the next $v$ to be $x$, so that $n < v^2$ (and $u$ doesn't change).

This dichotomy hints that maybe $u^2 \le n < v^2$ all the time. In other words, we suspect that it's a loop invariant. Verifying this is left as an exercise to the reader (remember to check that the property is true initially).

And now that we've done all this, we see that $u^2 \le n$ and $(u+1)^2 > n$: $u$ is the square root of $n$ rounded down to the nearest integer.

• "So you need to prove that u and v become equal in order to prove that the algorithm is correct" I think this sentence is missing a "not". – sepp2k Mar 13 '12 at 11:21
• @KenLi Since this is your question in the Stack Exchange sense, is there any particular improvement you'd like? – Gilles Mar 13 '12 at 21:34