examples/numeric/add_sqrt.mlw

   1 module AdditionSqrtSingle
   2   use real.RealInfix
   3   use real.Abs
   4   use ufloat.USingle
   5   use ufloat.USingleLemmas
   6   use ieee_float.RoundingMode
   7   use real.Square
   8
   9   val function usqrt (x:usingle) : usingle
  10
  11   let add_sqrt (a b : usingle)
  12     ensures {
  13       let exact = (to_real a +. to_real (usqrt b)) in
  14       abs (to_real result -. exact) <=. eps *. abs exact
  15     }
  16   = a ++. usqrt b
  17 end
  18
  19 module AdditionSqrtDouble
  20   use real.RealInfix
  21   use real.Abs
  22   use ufloat.UDouble
  23   use ufloat.UDoubleLemmas
  24   use ieee_float.RoundingMode
  25   use real.Square
  26
  27   val function usqrt (x:udouble) : udouble
  28
  29   let add_sqrt (a b : udouble)
  30     ensures {
  31       let exact = (to_real a +. to_real (usqrt b)) in
  32       abs (to_real result -. exact) <=. eps *. abs exact
  33     }
  34   = a ++. usqrt b
  35 end