why3/examples/binary_sqrt.mlw

(* 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