Commit 869b2542 authored by MARCHE Claude's avatar MARCHE Claude

added my_cosine example in regression tests (purely logic version)

parent c644c494
......@@ -145,7 +145,6 @@ why.conf
/tests/test-claude/
# /examples/
/examples/my_cosine/
/examples/genealogy/
/examples/programs/course/
/examples/programs/wcet_hull/
......
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import Rbasic_fun.
Require Import R_sqrt.
Require Import Rtrigo.
Require Import AltSeries. (* for def of pi *)
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), ((Rabs x) >= (0)%R)%R.
Axiom Sqrt_positive : forall (x:R), ((0)%R <= x)%R -> ((0)%R <= (sqrt x))%R.
Axiom Sqrt_positive : forall (x:R), (x >= (0)%R)%R -> ((sqrt x) >= (0)%R)%R.
Axiom Sqrt_square : forall (x:R), ((0)%R <= x)%R -> ((Rsqr (sqrt x)) = x).
Axiom Sqrt_square : forall (x:R), (x >= (0)%R)%R -> ((Rsqr (sqrt x)) = x).
Axiom Square_sqrt : forall (x:R), (x >= (0)%R)%R -> ((sqrt (x * x)%R) = x).
Axiom Square_sqrt : forall (x:R), ((0)%R <= x)%R -> ((sqrt (x * x)%R) = x).
Axiom Pythagorean_identity : forall (x:R),
(((Rsqr (Rtrigo_def.cos x)) + (Rsqr (Rtrigo_def.sin x)))%R = (1)%R).
......@@ -73,21 +62,18 @@ Axiom Sin_sum : forall (x:R) (y:R),
Parameter atan: R -> R.
Axiom Tan_atan : forall (x:R), ((Rtrigo.tan (atan x)) = x).
Inductive mode :=
| nearestTiesToEven : mode
| toZero : mode
| up : mode
| down : mode
| nearTiesToAway : mode .
| NearestTiesToEven : mode
| ToZero : mode
| Up : mode
| Down : mode
| NearTiesToAway : mode .
Parameter single : Type.
Definition max_single: R := (33554430 * 10141204801825835211973625643008)%R.
Definition max_int: Z := 16777216%Z.
Axiom Zero : ((IZR 0%Z) = (0)%R).
Axiom One : ((IZR 1%Z) = (1)%R).
......@@ -98,47 +84,53 @@ 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).
Axiom Neg : forall (x: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)) <= (max_single ))%R.
x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
Axiom Bounded_real_no_overflow : forall (m:mode) (x:R),
((Rabs x) <= (max_single ))%R -> (no_overflow m x).
((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),
(((-(max_int ))%Z <= i)%Z /\ (i <= (max_int ))%Z) -> ((round m
(((-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_down_le : forall (x:R), ((round (Down ) x) <= x)%R.
Axiom Round_up_ge : forall (x:R), ((round (up ) 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 )
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 )
Axiom Round_up_neg : forall (x:R), ((round (Up ) (-x)%R) = (-(round (Down )
x))%R).
Theorem MethodError : forall (x:R), ((Rabs x) <= (1 / 32)%R)%R ->
((Rabs (((1)%R - ((x * x)%R * (05 / 10)%R)%R)%R - (Rtrigo_def.cos x))%R) <= (1 / 16777216)%R)%R.
((Rabs (((1)%R - ((05 / 10)%R * (x * x)%R)%R)%R - (Rtrigo_def.cos x))%R) <= (1 / 16777216)%R)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x H.
Require Import Interval_tactic.
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/my_cosine/why3session.xml">
<file name="../my_cosine.why" verified="false" expanded="true">
<theory name="CosineSingle" verified="false" expanded="true">
<goal name="MethodError" sum="03308e96177082a1d3da02e1d9af1b90" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="my_cosine.why_CosineSingle_MethodError_1.v" obsolete="false">
<result status="valid" time="3.93"/>
</proof>
</goal>
<goal name="TotalErrorFullyExpanded" sum="2fc170302406d4bec35227d00816a288" proved="true" expanded="true">
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="TotalErrorExpanded" sum="aad0006d76fec58b87bf9c270f975fb4" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.81"/>
</proof>
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal name="TotalError" sum="0851711761327bfdfc8ed8a6b0c1fa03" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment