my_cosine.mlw 1.67 KB
Newer Older
1 2
module M

3 4 5 6 7
  use real.RealInfix
  use real.Abs
  use real.Trigonometry
  use floating_point.Rounding
  use floating_point.Single
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30

val single_of_real_exact : x:real ->
  { }
  single
  { value result = x }

val add : x:single -> y:single ->
  { no_overflow NearestTiesToEven ((value x) +. (value y)) }
  single
  { value result = round NearestTiesToEven ((value x) +. (value y))}

val sub : x:single -> y:single ->
  { no_overflow NearestTiesToEven ((value x) -. (value y)) }
  single
  { value result = round NearestTiesToEven ((value x) -. (value y))}

val mul : x:single -> y:single ->
  { no_overflow NearestTiesToEven ((value x) *. (value y)) }
  single
  { value result = round NearestTiesToEven ((value x) *. (value y))}


lemma method_error
31 32
    "expl:Lemma method_error"
    #"my_cosine.c" 1 4 111#
33
    :
34 35
    "expl:the formula"
    #"my_cosine.c" 1 24 110#
36 37
    forall x:real.
    abs x  <=. 0x1p-5 -> abs (1.0 -. x*.x*.0.5 -. cos x) <=. 0x1p-24
38

39
let my_cosine "expl:Safety of function my_cosine" #"my_cosine.c" 8 0 153#
40
    (x:single) : single =
41 42 43 44 45 46 47 48 49 50 51
{ abs (value x) <=. 0x1p-5 }
  assert {
    "expl:user assertion"
    #"my_cosine.c" 9 13 53#
    abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24
  };
  ("expl:check FP overflow for -"
   #"my_cosine.c" 10 9 28#
  sub (single_of_real_exact 1.0)
      ("expl:check FP overflow for *"
       #"my_cosine.c" 10 16 28#
52
       mul("expl:check FP overflow for second *"
53 54 55 56 57 58 59 60 61 62
           #"my_cosine.c" 10 16 21#
           mul x x) (single_of_real_exact 0.5)))
{ "expl:post-condition"
  #"my_cosine.c" 7 12 46#
  abs (value result -. cos (value x)) <=. 0x1p-23 }

end

(*
Local Variables:
63
compile-command: "../bin/why3ide.byte my_cosine.mlw"
64 65
End:
*)