examples_in_progress/my_exp.mlw

   1
   2 module ExpOld
   3
   4 end
   5
   6 module Exp
   7
   8   use ieee_float.Float64
   9   use real.Abs
  10   use real.ExpLog
  11   use real.Real
  12
  13   val ( +. ) (x y : t) : t
  14     requires {t'isFinite x}
  15     requires {t'isFinite y}
  16     requires {[@expl:no_overflow] t'isFinite (x .+ y)}
  17     ensures  {result = x .+ y}
  18
  19   val ( *. ) (x y : t) : t
  20     requires {t'isFinite x}
  21     requires {t'isFinite y}
  22     requires {[@expl:no_overflow] t'isFinite (x .* y)}
  23     ensures  {result = x .* y}
  24
  25   let my_exp (x: t) : t
  26     requires { t'isFinite x}
  27     requires { .- (1.0:t) .<= x .<= (1.0:t)}
  28     requires {abs (t'real x) <= 1.0}
  29     ensures { abs (t'real result - exp (t'real x)) <= 0x1p-4} (* 1 * 2 ^ - 4 *)
  30   =
  31     assert {
  32      let x = t'real x in
  33        abs(0.9890365552 + 1.130258690*x +
  34            0.5540440796*x*x - exp(x)) <= 0x0.FFFFp-4};
  35     (0x1.FA62FFD643D6Ep-1:t) +. (0x1.2158A22D91DE9p0:t) *. x +.
  36     (0x1.1BABAA64D94DBp-1:t) *. x *. x
  37
  38 end