Mentions légales du service

Skip to content
Snippets Groups Projects
Commit 43fbb552 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

updated proof sessions

parent ca1a168b
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 237 additions and 401 deletions
examples/TODO
+ 0
− 3
View file @ 43fbb552
...@@ -12,7 +12,6 @@ ewd673.mlw ...@@ -12,7 +12,6 @@ ewd673.mlw
fibonacci.mlw fibonacci.mlw
find.mlw find.mlw
finite_tarski.mlw finite_tarski.mlw
gcd_bezout.mlw
gcd.mlw gcd.mlw
hackers-delight.mlw hackers-delight.mlw
hashtbl_impl.mlw hashtbl_impl.mlw
...@@ -20,9 +19,7 @@ ieee_float.mlw ...@@ -20,9 +19,7 @@ ieee_float.mlw
kmp.mlw kmp.mlw
knuth_prime_numbers.mlw knuth_prime_numbers.mlw
koda_ruskey.mlw koda_ruskey.mlw
lcp.mlw
linked_list_rev.mlw linked_list_rev.mlw
my_cosine.mlw
optimal_replay.mlw optimal_replay.mlw
queens_bv.mlw queens_bv.mlw
queens.mlw queens.mlw
......
examples/gcd/why3session.xml
+ 80
− 138
View file @ 43fbb552
...@@ -3,198 +3,140 @@ ...@@ -3,198 +3,140 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="10" steplimit="0" memlimit="1000"/> <prover id="8" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.1" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.3" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../gcd.mlw" expanded="true"> <file name="../gcd.mlw" expanded="true">
<theory name="EuclideanAlgorithm" sum="993317fbd9660143d8a1f40de7e556d1"> <theory name="EuclideanAlgorithm" sum="06c09424aee65c6f411f277cd3f59aaf">
<goal name="WP_parameter euclid" expl="VC for euclid"> <goal name="VC euclid" expl="VC for euclid">
<transf name="split_goal_wp"> <proof prover="8"><result status="valid" time="4.32"/></proof>
<goal name="WP_parameter euclid.1" expl="1. postcondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="2" memlimit="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="2. check modulo by zero">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="3. variant decrease">
<proof prover="1" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="4. precondition">
<proof prover="1" memlimit="0"><result status="valid" time="0.02"/></proof>
<proof prover="5" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. postcondition">
<proof prover="0" timelimit="10" edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"><result status="valid" time="0.28"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="5" timelimit="10"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
</transf>
</goal> </goal>
</theory> </theory>
<theory name="EuclideanAlgorithmIterative" sum="e1e7cc66465c734015696eaa0de4e894"> <theory name="EuclideanAlgorithmIterative" sum="4841a879f96158e78cf1e196ec0e2c3b">
<goal name="WP_parameter euclid" expl="VC for euclid"> <goal name="VC euclid" expl="VC for euclid">
<transf name="split_goal_wp"> <proof prover="4"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter euclid.1" expl="1. loop invariant init">
<proof prover="5" timelimit="10"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter euclid.2" expl="2. check modulo by zero">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter euclid.3" expl="3. loop invariant preservation">
<proof prover="5" timelimit="10"><result status="valid" time="0.06" steps="20"/></proof>
</goal>
<goal name="WP_parameter euclid.4" expl="4. loop invariant preservation">
<proof prover="5" timelimit="10"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
<goal name="WP_parameter euclid.5" expl="5. loop variant decrease">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="30"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter euclid.6" expl="6. postcondition">
<proof prover="5" timelimit="10"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
</transf>
</goal> </goal>
</theory> </theory>
<theory name="BinaryGcd" sum="3c0323e27557f7bde78a916d38bcf9cf"> <theory name="BinaryGcd" sum="a78066797db663add80796b90f60375c" expanded="true">
<goal name="even1"> <goal name="even1">
<proof prover="5"><result status="valid" time="0.06" steps="18"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="19"/></proof>
</goal> </goal>
<goal name="odd1"> <goal name="odd1">
<proof prover="5"><result status="valid" time="0.06" steps="14"/></proof> <proof prover="9"><result status="valid" time="0.02" steps="21"/></proof>
</goal> </goal>
<goal name="div_nonneg"> <goal name="div_nonneg">
<proof prover="5"><result status="valid" time="0.02" steps="4"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="5"/></proof>
</goal> </goal>
<goal name="gcd_even_even"> <goal name="gcd_even_even">
<proof prover="5"><result status="valid" time="0.03" steps="28"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="29"/></proof>
</goal> </goal>
<goal name="gcd_even_odd"> <goal name="gcd_even_odd">
<proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="0.28"/></proof> <proof prover="0" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="0.28"/></proof>
</goal> </goal>
<goal name="gcd_even_odd2"> <goal name="gcd_even_odd2">
<proof prover="5"><result status="valid" time="0.17" steps="28"/></proof> <proof prover="9"><result status="valid" time="0.05" steps="29"/></proof>
</goal> </goal>
<goal name="odd_odd_div2"> <goal name="odd_odd_div2">
<proof prover="3"><result status="valid" time="0.01"/></proof> <proof prover="9"><result status="valid" time="0.63" steps="389"/></proof>
</goal> </goal>
<goal name="WP_parameter gcd_odd_odd" expl="VC for gcd_odd_odd"> <goal name="VC gcd_odd_odd" expl="VC for gcd_odd_odd">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.05" steps="31"/></proof> <proof prover="9"><result status="valid" time="0.02" steps="32"/></proof>
</goal> </goal>
<goal name="gcd_odd_odd2"> <goal name="gcd_odd_odd2">
<proof prover="5"><result status="valid" time="0.12" steps="24"/></proof> <proof prover="9"><result status="valid" time="0.07" steps="30"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd" expl="VC for binary_gcd"> <goal name="VC binary_gcd" expl="VC for binary_gcd" expanded="true">
<transf name="split_goal_wp"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter binary_gcd.1" expl="1. variant decrease"> <goal name="VC binary_gcd.1" expl="1. variant decrease">
<proof prover="4"><result status="valid" time="0.03"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="10"/></proof> </goal>
<goal name="VC binary_gcd.2" expl="2. precondition">
<proof prover="9"><result status="valid" time="0.01" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.2" expl="2. precondition"> <goal name="VC binary_gcd.3" expl="3. precondition">
<proof prover="4"><result status="valid" time="0.03"/></proof> <proof prover="9"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="6"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.3" expl="3. postcondition"> <goal name="VC binary_gcd.4" expl="4. precondition">
<proof prover="4"><result status="valid" time="0.02"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="6"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.4" expl="4. postcondition"> <goal name="VC binary_gcd.5" expl="5. check division by zero">
<proof prover="4"><result status="valid" time="0.03"/></proof> <proof prover="9"><result status="valid" time="0.00" steps="9"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="14"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.5" expl="5. check division by zero"> <goal name="VC binary_gcd.6" expl="6. check division by zero">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="9"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.6" expl="6. check division by zero"> <goal name="VC binary_gcd.7" expl="7. variant decrease">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="10"/></proof> <proof prover="9"><result status="valid" time="0.02" steps="33"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.7" expl="7. variant decrease"> <goal name="VC binary_gcd.8" expl="8. precondition">
<proof prover="5"><result status="valid" time="0.05" steps="24"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="17"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.8" expl="8. precondition"> <goal name="VC binary_gcd.9" expl="9. check division by zero">
<proof prover="4"><result status="valid" time="0.03"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="16"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.9" expl="9. postcondition"> <goal name="VC binary_gcd.10" expl="10. variant decrease">
<proof prover="1" timelimit="6"><result status="valid" time="0.02"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="4"><result status="valid" time="0.14"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.10" expl="10. check division by zero"> <goal name="VC binary_gcd.11" expl="11. precondition">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="9"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.11" expl="11. variant decrease"> <goal name="VC binary_gcd.12" expl="12. precondition">
<proof prover="5"><result status="valid" time="0.03" steps="20"/></proof> <proof prover="9"><result status="valid" time="0.00" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.12" expl="12. precondition"> <goal name="VC binary_gcd.13" expl="13. check division by zero">
<proof prover="4"><result status="valid" time="0.01"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="14"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.13" expl="13. postcondition"> <goal name="VC binary_gcd.14" expl="14. variant decrease">
<proof prover="4"><result status="valid" time="0.23"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.14" expl="14. check division by zero"> <goal name="VC binary_gcd.15" expl="15. precondition">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.02" steps="9"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.15" expl="15. variant decrease"> <goal name="VC binary_gcd.16" expl="16. check division by zero">
<proof prover="5"><result status="valid" time="0.04" steps="19"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.16" expl="16. precondition"> <goal name="VC binary_gcd.17" expl="17. variant decrease">
<proof prover="4"><result status="valid" time="0.01"/></proof> <proof prover="9"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="5"><result status="valid" time="0.02" steps="14"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.17" expl="17. postcondition"> <goal name="VC binary_gcd.18" expl="18. precondition">
<proof prover="4"><result status="valid" time="0.24"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="12"/></proof>
<proof prover="6"><result status="valid" time="0.05"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.18" expl="18. check division by zero"> <goal name="VC binary_gcd.19" expl="19. postcondition">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="9"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="8"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.19" expl="19. variant decrease"> <goal name="VC binary_gcd.20" expl="20. postcondition">
<proof prover="5"><result status="valid" time="0.08" steps="35"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="6"><result status="valid" time="0.15"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.20" expl="20. precondition"> <goal name="VC binary_gcd.21" expl="21. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="3.49"/></proof>
<proof prover="5"><result status="valid" time="0.03" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal> </goal>
<goal name="WP_parameter binary_gcd.21" expl="21. postcondition"> <goal name="VC binary_gcd.22" expl="22. postcondition" expanded="true">
<proof prover="4"><result status="valid" time="0.50"/></proof>
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="EuclideanAlgorithm31" sum="487d5bf6cabba374bf7b0237fee73e2c"> <theory name="EuclideanAlgorithm31" sum="9daace546ea2d1640762b559418142ef">
<goal name="WP_parameter euclid" expl="VC for euclid"> <goal name="VC euclid" expl="VC for euclid">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter euclid.1" expl="1. integer overflow"> <goal name="VC euclid.1" expl="1. integer overflow">
<proof prover="5" timelimit="5" memlimit="4000"><result status="valid" time="0.01" steps="3"/></proof> <proof prover="9"><result status="valid" time="0.00" steps="4"/></proof>
</goal> </goal>
<goal name="WP_parameter euclid.2" expl="2. postcondition"> <goal name="VC euclid.2" expl="2. division by zero">
<proof prover="7"><result status="valid" time="0.02" steps="13"/></proof> <proof prover="9"><result status="valid" time="0.00" steps="6"/></proof>
</goal> </goal>
<goal name="WP_parameter euclid.3" expl="3. division by zero"> <goal name="VC euclid.3" expl="3. integer overflow">
<proof prover="7"><result status="valid" time="0.01" steps="6"/></proof> <proof prover="9"><result status="valid" time="0.04" steps="49"/></proof>
</goal> </goal>
<goal name="WP_parameter euclid.4" expl="4. integer overflow"> <goal name="VC euclid.4" expl="4. variant decrease">
<proof prover="7"><result status="valid" time="0.07" steps="50"/></proof> <proof prover="9"><result status="valid" time="0.05" steps="54"/></proof>
</goal> </goal>
<goal name="WP_parameter euclid.5" expl="5. variant decrease"> <goal name="VC euclid.5" expl="5. precondition">
<proof prover="7"><result status="valid" time="0.50" steps="169"/></proof> <proof prover="9"><result status="valid" time="0.00" steps="15"/></proof>
</goal> </goal>
<goal name="WP_parameter euclid.6" expl="6. precondition"> <goal name="VC euclid.6" expl="6. postcondition">
<proof prover="7"><result status="valid" time="0.02" steps="22"/></proof> <proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
</goal> </goal>
<goal name="WP_parameter euclid.7" expl="7. postcondition"> <goal name="VC euclid.7" expl="7. postcondition">
<proof prover="7"><result status="valid" time="0.11" steps="41"/></proof> <proof prover="9"><result status="valid" time="0.02" steps="29"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
examples/gcd/why3shapes.gz
+ 0
− 0
View file @ 43fbb552
No preview for this file type
examples/gcd_bezout/why3session.xml
+ 0
− 1
View file @ 43fbb552
...@@ -31,7 +31,6 @@ ...@@ -31,7 +31,6 @@
</goal> </goal>
<goal name="VC gcd.8" expl="8. loop variant decrease"> <goal name="VC gcd.8" expl="8. loop variant decrease">
<proof prover="2"><result status="valid" time="0.04"/></proof> <proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="4"><undone/></proof>
</goal> </goal>
<goal name="VC gcd.9" expl="9. loop invariant preservation"> <goal name="VC gcd.9" expl="9. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.18" steps="42"/></proof> <proof prover="4"><result status="valid" time="0.18" steps="42"/></proof>
......
examples/kmp/why3session.xml
+ 136
− 193
View file @ 43fbb552
This diff is collapsed.
examples/kmp/why3shapes.gz
+ 0
− 0
View file @ 43fbb552
No preview for this file type
examples/lcp/why3session.xml
+ 5
− 48
View file @ 43fbb552
...@@ -2,57 +2,14 @@ ...@@ -2,57 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="2" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="5" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../lcp.mlw" expanded="true"> <file name="../lcp.mlw" expanded="true">
<theory name="LCP" sum="b7b041689ff58a3f4d1518790558ac63" expanded="true"> <theory name="LCP" sum="50feeeaf6717c74702bac9e115a2b860" expanded="true">
<goal name="not_eqseq" expanded="true"> <goal name="not_eqseq" expanded="true">
<proof prover="4"><result status="valid" time="0.02" steps="9"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
</goal> </goal>
<goal name="WP_parameter lcp" expl="VC for lcp" expanded="true"> <goal name="VC lcp" expl="VC for lcp" expanded="true">
<transf name="split_goal_wp" expanded="true"> <proof prover="0"><result status="valid" time="0.02" steps="79"/></proof>
<goal name="WP_parameter lcp.1" expl="1. loop invariant init">
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter lcp.2" expl="2. index in array bounds">
<proof prover="4"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter lcp.3" expl="3. index in array bounds">
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter lcp.4" expl="4. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter lcp.5" expl="5. loop variant decrease">
<proof prover="4"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter lcp.6" expl="6. postcondition">
<proof prover="4"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter lcp.7" expl="7. postcondition" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="WP_parameter lcp.7.1" expl="1. postcondition" expanded="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.18"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter lcp.8" expl="8. postcondition">
<proof prover="4"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter lcp.9" expl="9. postcondition">
<proof prover="4"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter lcp.10" expl="10. postcondition">
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter lcp.11" expl="11. postcondition">
<proof prover="4" timelimit="5"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
</goal> </goal>
</theory> </theory>
</file> </file>
......
examples/lcp/why3shapes.gz
+ 0
− 0
View file @ 43fbb552
No preview for this file type
examples/my_cosine/my_cosine_M_WP_parameter_my_cosine_1.v → examples/my_cosine/my_cosine_M_VC_my_cosine_1.v
+ 2
− 5
View file @ 43fbb552
...@@ -23,14 +23,11 @@ Definition unit := unit. ...@@ -23,14 +23,11 @@ Definition unit := unit.
Require Import Interval.Interval_tactic. Require Import Interval.Interval_tactic.
(* Why3 goal *) (* Why3 goal *)
Theorem WP_parameter_my_cosine : forall (x:floating_point.SingleFormat.single), Theorem VC_my_cosine : forall (x:floating_point.SingleFormat.single),
((Reals.Rbasic_fun.Rabs (floating_point.Single.value x)) <= (1 / 32)%R)%R -> ((Reals.Rbasic_fun.Rabs (floating_point.Single.value x)) <= (1 / 32)%R)%R ->
((Reals.Rbasic_fun.Rabs ((1%R - (((floating_point.Single.value x) * (floating_point.Single.value x))%R * (05 / 10)%R)%R)%R - (Reals.Rtrigo_def.cos (floating_point.Single.value x)))%R) <= (1 / 16777216)%R)%R. ((Reals.Rbasic_fun.Rabs ((1%R - (((floating_point.Single.value x) * (floating_point.Single.value x))%R * (05 / 10)%R)%R)%R - (Reals.Rtrigo_def.cos (floating_point.Single.value x)))%R) <= (1 / 16777216)%R)%R.
(* Why3 intros x h1. *) intros x h1.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x H.
interval with (i_bisect_diff (Single.value x)). interval with (i_bisect_diff (Single.value x)).
Qed. Qed.
examples/my_cosine/why3session.xml
+ 14
− 13
View file @ 43fbb552
...@@ -2,28 +2,29 @@ ...@@ -2,28 +2,29 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="Gappa" version="1.3.0" timelimit="2" steplimit="0" memlimit="0"/> <prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../my_cosine.mlw" expanded="true"> <file name="../my_cosine.mlw" expanded="true">
<theory name="M" sum="e6984a9af2ab6c45ac0e8af4e992df4e" expanded="true"> <theory name="M" sum="9703bc37ded6a61396b1df1dc41b18d6" expanded="true">
<goal name="WP_parameter my_cosine" expl="VC for my_cosine" expanded="true"> <goal name="VC my_cosine" expl="VC for my_cosine" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="1. assertion" expanded="true"> <goal name="VC my_cosine.1" expl="1. assertion" expanded="true">
<proof prover="2"><result status="valid" time="0.17"/></proof> <proof prover="2"><result status="valid" time="0.14"/></proof>
<proof prover="3" edited="my_cosine_M_WP_parameter_my_cosine_1.v"><result status="valid" time="1.79"/></proof> <proof prover="3" edited="my_cosine_M_VC_my_cosine_1.v"><result status="valid" time="1.79"/></proof>
</goal> </goal>
<goal name="WP_parameter my_cosine.2" expl="2. precondition" expanded="true"> <goal name="VC my_cosine.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.00"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal> </goal>
<goal name="WP_parameter my_cosine.3" expl="3. precondition" expanded="true"> <goal name="VC my_cosine.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.00"/></proof> <proof prover="1"><result status="valid" time="0.05" steps="188"/></proof>
</goal> </goal>
<goal name="WP_parameter my_cosine.4" expl="4. precondition" expanded="true"> <goal name="VC my_cosine.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.00"/></proof> <proof prover="0"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="WP_parameter my_cosine.5" expl="5. postcondition" expanded="true"> <goal name="VC my_cosine.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.00"/></proof> <proof prover="0"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
examples/my_cosine/why3shapes.gz
+ 0
− 0
View file @ 43fbb552
No preview for this file type
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment