exemple of cosine

.gitignore

+*~
 *.o
 *.svn
 .*.swp

examples/programs/my_cosine.mlw

+
+{
+
+  use import real.RealInfix
+  use import real.Abs
+  use import real.Trigonometry
+  use import floating_point.Rounding
+  use import floating_point.Single
+
+}
+
+parameter single_of_real_exact : x:real ->
+  { }
+  single
+  { value result = x }
+
+parameter add : x:single -> y:single ->
+  { no_overflow NearestTiesToEven ((value x) +. (value y)) }
+  single
+  { value result = round NearestTiesToEven ((value x) +. (value y))}
+
+parameter sub : x:single -> y:single ->
+  { no_overflow NearestTiesToEven ((value x) -. (value y)) }
+  single
+  { value result = round NearestTiesToEven ((value x) -. (value y))}
+
+parameter mul : x:single -> y:single ->
+  { no_overflow NearestTiesToEven ((value x) *. (value y)) }
+  single
+  { value result = round NearestTiesToEven ((value x) *. (value y))}
+
+
+let my_cosine (x:single) : single =
+{ abs (value x) <=. 0x1p-5 }
+  assert { 
+    abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24 
+  };
+  sub (single_of_real_exact 1.0)
+      (mul (mul x x) (single_of_real_exact 0.5))
+{ abs (value result -. cos (value x)) <=. 0x1p-23 }
+
+(*
+Local Variables:
+compile-command: "../../bin/whydb.byte my_cosine.mlw"
+End:
+*)
+
+

examples/programs/my_cosine/my_cosine.mlw_Pgm_WP_my_cosine.v

+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import Rbasic_fun.
+Require Import R_sqrt.
+Require Import Rtrigo.
+Require Import AltSeries.
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+Implicit Arguments ignore.
+
+Parameter arrow : forall (a:Type) (b:Type), Type.
+
+Parameter ref : forall (a:Type), Type.
+
+Parameter prefix_ex: forall (a:Type), (ref a)  -> a.
+Implicit Arguments prefix_ex.
+
+Parameter label : Type.
+
+Parameter at1: forall (a:Type), a -> label  -> a.
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+Implicit Arguments old.
+
+Parameter exn : Type.
+
+Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x <  y)%Z.
+
+Axiom Refl : forall (x:R), (x <= x)%R.
+
+Axiom Trans : forall (x:R) (y:R) (z:R), (x <= y)%R -> ((y <= z)%R ->
+  (x <= z)%R).
+
+Axiom Antisymm : forall (x:R) (y:R), (x <= y)%R -> ((y <= x)%R -> (x = y)).
+
+Axiom Total : forall (x:R) (y:R), (x <= y)%R \/ (y <= x)%R.
+
+Axiom Abs_le : forall (x:R) (y:R), ((Rabs x) <= y)%R <-> (((-y)%R <= x)%R /\
+  (x <= y)%R).
+
+Axiom Abs_pos : forall (x:R), ((0)%R <= (Rabs x))%R.
+
+Axiom Sqrt_positive : forall (x:R), ((0)%R <= x)%R -> ((0)%R <= (sqrt x))%R.
+
+Axiom Sqrt_square : forall (x:R), ((0)%R <= x)%R ->
+  (((sqrt x) * (sqrt x))%R = x).
+
+Axiom Square_sqrt : forall (x:R), ((0)%R <= x)%R -> ((sqrt (x * x)%R) = x).
+
+Axiom Pythagorean_identity : forall (x:R),
+  ((((cos x) * (cos x))%R + ((sin x) * (sin x))%R)%R = (1)%R).
+
+Axiom Cos_le_one : forall (x:R), ((Rabs (cos x)) <= (1)%R)%R.
+
+Axiom Sin_le_one : forall (x:R), ((Rabs (sin x)) <= (1)%R)%R.
+
+Axiom Cos_0 : ((cos (0)%R) = (1)%R).
+
+Axiom Sin_0 : ((sin (0)%R) = (0)%R).
+
+Axiom Pi_interval : ((314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R <  PI)%R /\
+  (PI <  (314159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 / 100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%R)%R.
+
+Axiom Cos_pi : ((cos PI) = (-(1)%R)%R).
+
+Axiom Sin_pi : ((sin PI) = (0)%R).
+
+Axiom Cos_pi2 : ((cos ((05 / 10)%R * PI)%R) = (0)%R).
+
+Axiom Sin_pi2 : ((sin ((05 / 10)%R * PI)%R) = (1)%R).
+
+Axiom Cos_plus_pi : forall (x:R), ((cos (x + PI)%R) = (-(cos x))%R).
+
+Axiom Sin_plus_pi : forall (x:R), ((sin (x + PI)%R) = (-(sin x))%R).
+
+Axiom Cos_plus_pi2 : forall (x:R),
+  ((cos (x + ((05 / 10)%R * PI)%R)%R) = (-(sin x))%R).
+
+Axiom Sin_plus_pi2 : forall (x:R),
+  ((sin (x + ((05 / 10)%R * PI)%R)%R) = (cos x)).
+
+Axiom Cos_neg : forall (x:R), ((cos (-x)%R) = (cos x)).
+
+Axiom Sin_neg : forall (x:R), ((sin (-x)%R) = (-(sin x))%R).
+
+Axiom Cos_sum : forall (x:R) (y:R),
+  ((cos (x + y)%R) = (((cos x) * (cos y))%R - ((sin x) * (sin y))%R)%R).
+
+Axiom Sin_sum : forall (x:R) (y:R),
+  ((sin (x + y)%R) = (((sin x) * (cos y))%R + ((cos x) * (sin y))%R)%R).
+
+Parameter atan: R  -> R.
+
+Axiom Tan_atan : forall (x:R), ((tan (atan x)) = x).
+
+Inductive mode  :=
+  | nearestTiesToEven : mode 
+  | toZero : mode 
+  | up : mode 
+  | down : mode 
+  | nearTiesToAway : mode .
+
+Parameter single : Type.
+
+Axiom Zero : ((IZR 0%Z) = (0)%R).
+
+Axiom One : ((IZR 1%Z) = (1)%R).
+
+Axiom Add : forall (x:Z) (y:Z), ((IZR (x + y)%Z) = ((IZR x) + (IZR y))%R).
+
+Axiom Sub : forall (x:Z) (y:Z), ((IZR (x - y)%Z) = ((IZR x) - (IZR y))%R).
+
+Axiom Mul : forall (x:Z) (y:Z), ((IZR (x * y)%Z) = ((IZR x) * (IZR y))%R).
+
+Axiom Neg : forall (x:Z) (y:Z), ((IZR (-x)%Z) = (-(IZR x))%R).
+
+Parameter round: mode -> R  -> R.
+
+Parameter round_logic: mode -> R  -> single.
+
+Parameter value: single  -> R.
+
+Parameter exact: single  -> R.
+
+Parameter model: single  -> R.
+
+Definition round_error(x:single): R := (Rabs ((value x) - (exact x))%R).
+
+Definition total_error(x:single): R := (Rabs ((value x) - (model x))%R).
+
+Definition no_overflow(m:mode) (x:R): Prop := ((Rabs (round m
+  x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
+
+Axiom Bounded_real_no_overflow : forall (m:mode) (x:R),
+  ((Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
+  (no_overflow m x).
+
+Axiom Round_monotonic : forall (m:mode) (x:R) (y:R), (x <= y)%R -> ((round m
+  x) <= (round m y))%R.
+
+Axiom Exact_rounding_for_integers : forall (m:mode) (i:Z),
+  (((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z) -> ((round m
+  (IZR i)) = (IZR i)).
+
+Axiom Round_down_le : forall (x:R), ((round (down ) x) <= x)%R.
+
+Axiom Round_up_ge : forall (x:R), (x <= (round (up ) x))%R.
+
+Axiom Round_down_neg : forall (x:R), ((round (down ) (-x)%R) = (-(round (up )
+  x))%R).
+
+Axiom Round_up_neg : forall (x:R), ((round (up ) (-x)%R) = (-(round (down )
+  x))%R).
+
+Theorem WP_my_cosine : forall (x:single),
+  ((Rabs (value x)) <= (1 / 32)%R)%R ->
+  ((Rabs (((1)%R - (((value x) * (value x))%R * (05 / 10)%R)%R)%R - (cos (value x)))%R) <= (1 / 16777216)%R)%R.
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros x Hx.
+Require Import Interval_tactic.
+interval with (i_bisect_diff (value x)).
+Qed.
+(* DO NOT EDIT BELOW *)
+
+