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.