Proving correctness of the Newton's Method for finding the square root of a number

I'm trying to prove the correctness of this simple square root calculation algorithm using SPARK:

Y := X / 2.0;
while abs (X - Y ** 2) > Tol * X loop
Y := 0.5 * (Y + X / Y);
end loop;
return Y;

The preconditions are that both X and Tol are greater then zero and the postcondition is simply the opposite of the while loop's condition.

Are there any invariants of the loop above that may help? Or maybe a different algorithm (eg. bisection) would be a better choice? So far I've tried showing that the value of the square root is always between Y and X / Y but that didn't get me anywhere.

• I suggest you try to prove the correctness of the algorithm (using infinite-precision math) first, before you try to figure out how to apply that to SPARK code or to deal with the imprecision of floating-point arithmetic. Do you know how to prove Newton's method correct? If not, perhaps it'd be worthwhile to do some research on that (try a numerical methods textbook), and if you still can't find anything on that, ask a new question about that. – D.W. Mar 16 at 18:55
• You should check out this. – ryan Apr 16 at 18:19