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.