Commit aa554a31 authored by MARCHE Claude's avatar MARCHE Claude

update proofs of my_cosine.why

parent eefb88cd
......@@ -11,16 +11,16 @@ use import floating_point.Single
lemma MethodError: forall x:real. abs x <= 0x1p-5 ->
abs (1.0 - 0.5 * (x * x) - cos x) <= 0x1p-24
(* this one is proved in Coq + interval tactics *)
abs (1.0 - 0.5 * (x * x) - cos x) <= 0x1p-24
(* this one is proved in Coq + interval tactics *)
(* computation in single precision *)
lemma TotalErrorFullyExpanded:
lemma TotalErrorFullyExpanded:
forall x:single. abs (value x) <= 0x1p-5 ->
(* total error as hypothesis, for Gappa *)
abs (1.0 - 0.5 * (value x * value x) - cos (value x)) <= 0x1p-24 ->
abs (1.0 - 0.5 * (value x * value x) - cos (value x)) <= 0x1p-24 ->
forall x2 x2o2 cos_x: real.
x2 = round NearestTiesToEven (value x * value x) ->
x2o2 = round NearestTiesToEven (0.5 * x2) ->
......@@ -28,7 +28,7 @@ lemma TotalErrorFullyExpanded:
abs (cos_x - cos (value x)) <= 0x1p-23
(* fully expanded version, proved by gappa *)
lemma TotalErrorExpanded:
lemma TotalErrorExpanded:
forall x:single. abs (value x) <= 0x1p-5 ->
let x2 = round NearestTiesToEven (value x * value x) in
let x2o2 = round NearestTiesToEven (0.5 * x2) in
......@@ -40,13 +40,13 @@ lemma TotalErrorExpanded:
function round_single (m:mode) (x:real) : single
axiom RoundSingle: forall m:mode, x:real.
axiom RoundSingle: forall m:mode, x:real [value (round_single m x)].
value (round_single m x) = round m x
function cos_single (x:single) : single =
let x2 = round_single NearestTiesToEven (value x * value x) in
let x2o2 = round_single NearestTiesToEven (0.5 * value x2) in
round_single NearestTiesToEven (1.0 - value x2o2)
round_single NearestTiesToEven (1.0 - value x2o2)
lemma TotalError: forall x:single. abs (value x) <= 0x1p-5 ->
let cos_x = cos_single x in
......@@ -57,7 +57,7 @@ end
(*
Local Variables:
compile-command: "../bin/whyide.byte my_cosine.why"
compile-command: "../bin/why3ide.byte my_cosine.why"
End:
*)
......
<?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">
<why3session name="my_cosine/why3session.xml">
<file name="../my_cosine.why" verified="true" expanded="true">
<theory name="CosineSingle" verified="true" expanded="true">
<goal name="MethodError" sum="04d7ba2ad67e6273c77266e812fe0b5d" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="my_cosine_CosineSingle_MethodError_1.v" obsolete="false">
<result status="valid" time="3.93"/>
<result status="valid" time="4.29"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.04"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
</proof>
</goal>
<goal name="TotalErrorFullyExpanded" sum="2fc170302406d4bec35227d00816a288" proved="true" expanded="true">
<goal name="TotalErrorFullyExpanded" sum="86136c1aa7501342a2789f26b4088e3b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.01"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.09"/>
</proof>
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
</proof>
</goal>
<goal name="TotalErrorExpanded" sum="aad0006d76fec58b87bf9c270f975fb4" proved="true" expanded="true">
<goal name="TotalErrorExpanded" sum="1d2075874f81d542bc1500ae6147faec" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.81"/>
<result status="valid" time="0.98"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
<result status="valid" time="0.12"/>
</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.09"/>
<goal name="TotalError" sum="84d328c047b191246fda42eaa2ab5255" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="2.73"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.69"/>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.12"/>
</proof>
</goal>
</theory>
......
......@@ -728,8 +728,10 @@ let (_ : GMenu.image_menu_item) =
let refresh_provers = ref (fun () -> ())
let add_refresh_provers f msg =
let add_refresh_provers f _msg =
(*
eprintf "[Info] recording '%s' for refresh provers@." msg;
*)
let rp = !refresh_provers in
refresh_provers := (fun () -> rp (); f ())
......
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