tests/my_cosine.mlw

   1 module M
   2
   3   use real.RealInfix
   4   use real.Abs
   5   use real.Trigonometry
   6   use floating_point.Rounding
   7   use floating_point.Single
   8
   9 val single_of_real_exact : x:real ->
  10   { }
  11   single
  12   { value result = x }
  13
  14 val add : x:single -> y:single ->
  15   { no_overflow NearestTiesToEven ((value x) +. (value y)) }
  16   single
  17   { value result = round NearestTiesToEven ((value x) +. (value y))}
  18
  19 val sub : x:single -> y:single ->
  20   { no_overflow NearestTiesToEven ((value x) -. (value y)) }
  21   single
  22   { value result = round NearestTiesToEven ((value x) -. (value y))}
  23
  24 val mul : x:single -> y:single ->
  25   { no_overflow NearestTiesToEven ((value x) *. (value y)) }
  26   single
  27   { value result = round NearestTiesToEven ((value x) *. (value y))}
  28
  29
  30 lemma method_error
  31     "expl:Lemma method_error"
  32     #"my_cosine.c" 1 4 111#
  33     :
  34     "expl:the formula"
  35     #"my_cosine.c" 1 24 110#
  36     forall x:real.
  37     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 { abs (value x) <=. 0x1p-5 }
  42   assert {
  43     "expl:user assertion"
  44     #"my_cosine.c" 9 13 53#
  45     abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24
  46   };
  47   ("expl:check FP overflow for -"
  48    #"my_cosine.c" 10 9 28#
  49   sub (single_of_real_exact 1.0)
  50       ("expl:check FP overflow for *"
  51        #"my_cosine.c" 10 16 28#
  52        mul("expl:check FP overflow for second *"
  53            #"my_cosine.c" 10 16 21#
  54            mul x x) (single_of_real_exact 0.5)))
  55 { "expl:post-condition"
  56   #"my_cosine.c" 7 12 46#
  57   abs (value result -. cos (value x)) <=. 0x1p-23 }
  58
  59 end
  60
  61 (*
  62 Local Variables:
  63 compile-command: "../bin/why3ide.byte my_cosine.mlw"
  64 End:
  65 *)