Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
2  
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
add comment

Know someone who can answer? Share a link to this question via email, Google+, Twitter, or Facebook.

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.