## Binary Square Root

Computing the square root (up to eps) using binary search

Authors: Jean-Christophe Filliâtre

Topics: Arithmetic / Non-linear Arithmetic

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

```(* Computing the square root (up to eps) using binary search

Note: precondition 0. < eps is not necessary for soundness
but needed to ensure termination.
*)

module BinarySqrt

use real.Real
use int.Int as Int
use real.MinMax as MinMax
use real.FromInt as FromInt
use real.Truncate as Truncate

let rec sqrt (r: real) (eps: real) (ghost n:int) (ghost eps0:real) : real
requires { 0.0 <= r }
requires { eps0 > 0.0 /\ Int.(>=) n 1 }
requires { eps = (FromInt.from_int n) * eps0 }
variant  { Int.(-) (Truncate.ceil (MinMax.max r 1.0 / eps0)) n }
ensures  { result * result <= r < (result + eps) * (result + eps) }
= if r < eps && 1.0 < eps then
0.0
else
begin
assert { FromInt.from_int n * eps0 <= MinMax.max r 1.0 };
assert { 1.0 / eps0 > 0.0 };
assert { FromInt.from_int n * eps0 * (1.0 / eps0) <= MinMax.max r 1.0 * (1.0 / eps0)};
assert { FromInt.from_int n * eps0 / eps0 <= MinMax.max r 1.0 / eps0};
assert { FromInt.from_int n <= MinMax.max r 1.0 / eps0 };
let r' = sqrt r (2.0 * eps) (Int.(*) 2 n) eps0 in
if (r' + eps) * (r' + eps) <= r then r' + eps else r'
end

let sqrt_main (r:real) (eps:real) : real
requires { 0.0 <= r }
requires { eps > 0.0 }
ensures  { result * result <= r < (result + eps) * (result + eps) }
= sqrt r eps 1 eps

end
```