my_cosine.mlw 1.12 KB
Newer Older
1 2 3 4 5

(* Approximated cosine

   Claude Marché (Inria) *)

6
module M
Claude Marche's avatar
Claude Marche committed
7 8 9 10 11 12 13

  use import real.RealInfix
  use import real.Abs
  use import real.Trigonometry
  use import floating_point.Rounding
  use import floating_point.Single

14 15
val single_of_real_exact (x: real) : single
  ensures { value result = x }
Claude Marche's avatar
Claude Marche committed
16

17 18 19
val add (x y: single) : single
  requires { no_overflow NearestTiesToEven ((value x) +. (value y)) }
  ensures  { value result = round NearestTiesToEven ((value x) +. (value y))}
Claude Marche's avatar
Claude Marche committed
20

21 22 23
val sub (x y: single) : single
  requires { no_overflow NearestTiesToEven ((value x) -. (value y)) }
  ensures  { value result = round NearestTiesToEven ((value x) -. (value y))}
Claude Marche's avatar
Claude Marche committed
24

25 26 27
val mul (x y: single) : single
  requires { no_overflow NearestTiesToEven ((value x) *. (value y)) }
  ensures  { value result = round NearestTiesToEven ((value x) *. (value y))}
Claude Marche's avatar
Claude Marche committed
28

29 30 31 32
let my_cosine (x:single) : single
  requires { abs (value x) <=. 0x1p-5 }
  ensures { abs (value result -. cos (value x)) <=. 0x1p-23 }
= assert {
33
    abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24
Claude Marche's avatar
Claude Marche committed
34
  };
35
  sub (single_of_real_exact 1.0) (mul (mul x x) (single_of_real_exact 0.5))
Claude Marche's avatar
Claude Marche committed
36

37
end