examples/my_cosine.mlw

   1
   2 (* Approximated cosine
   3
   4    Claude Marché (Inria) *)
   5
   6 module M
   7
   8   use real.RealInfix
   9   use real.Abs
  10   use real.Trigonometry
  11   use floating_point.Rounding
  12   use floating_point.Single
  13
  14 val single_of_real_exact (x: real) : single
  15   ensures { value result = x }
  16
  17 val add (x y: single) : single
  18   requires { no_overflow NearestTiesToEven ((value x) +. (value y)) }
  19   ensures  { value result = round NearestTiesToEven ((value x) +. (value y))}
  20
  21 val sub (x y: single) : single
  22   requires { no_overflow NearestTiesToEven ((value x) -. (value y)) }
  23   ensures  { value result = round NearestTiesToEven ((value x) -. (value y))}
  24
  25 val mul (x y: single) : single
  26   requires { no_overflow NearestTiesToEven ((value x) *. (value y)) }
  27   ensures  { value result = round NearestTiesToEven ((value x) *. (value y))}
  28
  29 let my_cosine (x:single) : single
  30   requires { abs (value x) <=. 0x1p-5 }
  31   ensures { abs (value result -. cos (value x)) <=. 0x1p-23 }
  32 = assert {
  33     abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24
  34   };
  35   sub (single_of_real_exact 1.0) (mul (mul x x) (single_of_real_exact 0.5))
  36
  37 end