examples_in_progress/exp.mlw

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