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) &gt; 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 take some example values and see the pattern how Y actually changes. Observe that at the first iteration of the loop, Y may be too small, but only on the first iteration. Then you should see how Y changes after that. 

With that, you should find a much stronger loop invariant that lets you actually prove convergence (if TOL is small enough and we ignore arithmetic overflow).