1
$\begingroup$

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.

Improve this question
$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – D.W.♦ Mar 16 '19 at 18:55
  • $\begingroup$ You should check out this. $\endgroup$ – ryan Apr 16 '19 at 18:19
0
$\begingroup$

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).

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.