Skip to content

GitLab

why3
why3
Commit aee107f3 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

updated proofs on moloch

parent 94179377
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 216 additions and 205 deletions
examples/programs/decrease1/why3session.xml
View file @ aee107f3
This diff is collapsed.
examples/programs/euler001/why3session.xml
View file @ aee107f3
......@@ -14,7 +14,7 @@
<result status="unknown" time="0.06"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.38"/>
<result status="unknown" time="4.31"/>
</proof>
</goal>
<goal name="div_minus1_2" sum="58b4c2b7cc926f7281ef2d9806046849" proved="false" expanded="true">
......@@ -28,10 +28,10 @@
<result status="unknown" time="0.04"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
<result status="unknown" time="1.45"/>
</proof>
</goal>
<goal name="mod_15" sum="e2d678bf333354c7d41e3255a00ce78b" proved="true" expanded="false">
<goal name="mod_15" sum="e2d678bf333354c7d41e3255a00ce78b" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
......@@ -42,7 +42,7 @@
<result status="valid" time="0.44"/>
</proof>
</goal>
<goal name="Closed_formula_0" sum="bedb2551f46c9bf80e4fd6d1cddcc221" proved="true" expanded="false">
<goal name="Closed_formula_0" sum="bedb2551f46c9bf80e4fd6d1cddcc221" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
......@@ -53,7 +53,7 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Closed_formula_n_1" sum="07cd7a1e0916a0fd5db441ad655752d4" proved="true" expanded="false">
<goal name="Closed_formula_n_1" sum="07cd7a1e0916a0fd5db441ad655752d4" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.17"/>
</proof>
......@@ -72,28 +72,25 @@
<result status="timeout" time="2.09"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
<result status="timeout" time="5.08"/>
</proof>
</goal>
<goal name="Closed_formula" sum="6a9095ec398278b6e7fa407e16f64039" proved="true" expanded="false">
<goal name="Closed_formula" sum="6a9095ec398278b6e7fa407e16f64039" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</theory>
<theory name="Euler001" verified="true" expanded="false">
<goal name="WP_parameter solve" expl="normal postcondition" sum="c41d9ff50a1fcc7bd5f7a82e94c058f3" proved="true" expanded="false">
<theory name="Euler001" verified="true" expanded="true">
<goal name="WP_parameter solve" expl="normal postcondition" sum="dd6f0e34463bcfbf4b3ca11577b727c6" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.68"/>
<result status="valid" time="0.46"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.16"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
</theory>
......
examples/programs/gcd/why3session.xml
View file @ aee107f3
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/gcd/why3session.xml">
<why3session name="examples/programs/gcd/why3session.xml">
<file name="../gcd.mlw" verified="false" expanded="true">
<theory name="M" verified="false" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="665cff5a35980903b7a8eb517c404e17" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.34"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="13686aa7223ccd074e11892070fa497c" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter gcd.1" expl="normal postcondition" sum="d6c14b7052f661d1db3c5517270a214e" proved="true" expanded="true">
<goal name="WP_parameter gcd.1" expl="normal postcondition" sum="e04458a1deb8f46c32e2040984924ab2" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.65"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2" expl="precondition" sum="ac183d41241c6eaf028e3626e0097b97" proved="true" expanded="true">
<goal name="WP_parameter gcd.2" expl="precondition" sum="b1c7e0b73a7e08e9bfb9e73aa85762d7" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.3" expl="normal postcondition" sum="7e7d74481a07874402868ca8e73fb044" proved="false" expanded="true">
<goal name="WP_parameter gcd.3" expl="normal postcondition" sum="c0a0f540fca852dd68a554221754e076" proved="false" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="1.16"/>
<result status="unknown" time="1.08"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.42"/>
<result status="unknown" time="0.48"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
<result status="timeout" time="2.09"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.08"/>
<result status="timeout" time="2.09"/>
</proof>
</goal>
</transf>
......
examples/programs/gcd_bezout/why3session.xml
View file @ aee107f3
......@@ -3,77 +3,68 @@
<why3session name="examples/programs/gcd_bezout/why3session.xml">
<file name="../gcd_bezout.mlw" verified="false" expanded="true">
<theory name="M" verified="false" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="44c73ab6d7cb8f3f8241f534deb156f1" proved="false" expanded="true">
<goal name="WP_parameter gcd" expl="correctness of parameter gcd" sum="66a8795f899d84ac0583a005fe89ce0a" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter gcd.1" expl="loop invariant init" sum="8566a02a986fda736b7f696339e845f1" proved="true" expanded="true">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<goal name="WP_parameter gcd.1" expl="loop invariant init" sum="131bc5920f4ba44c45ffaa828fa737f7" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2" expl="loop invariant preservation" sum="6aa9c41319e3ce9cdb5c07f21e43fc1a" proved="false" expanded="true">
<goal name="WP_parameter gcd.2" expl="loop invariant preservation" sum="40aa1567edcd01c99aa5393619f44a10" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter gcd.2.1" expl="correctness of parameter gcd" sum="2bf2b9018cef97e7d6861be9a099632c" proved="true" expanded="true">
<goal name="WP_parameter gcd.2.1" expl="correctness of parameter gcd" sum="387342c4c6c376ec84db024d590eb931" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.2" expl="correctness of parameter gcd" sum="134839062fcb2bdd8f91686991426f7d" proved="true" expanded="true">
<goal name="WP_parameter gcd.2.2" expl="correctness of parameter gcd" sum="e481d13a9bd5964ad8928b356e7918b2" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.3" expl="correctness of parameter gcd" sum="77ed7e7e438dca7dc5d795505d376a85" proved="false" expanded="true">
<goal name="WP_parameter gcd.2.3" expl="correctness of parameter gcd" sum="6e74075706d766eaefd70566ef1c7992" proved="false" expanded="true">
<proof prover="simplify" timelimit="3" edited="" obsolete="false">
<result status="timeout" time="3.09"/>
<result status="timeout" time="3.08"/>
</proof>
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="timeout" time="3.08"/>
<result status="unknown" time="0.11"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.05"/>
<result status="timeout" time="10.03"/>
</proof>
<proof prover="z3" timelimit="3" edited="" obsolete="false">
<result status="timeout" time="3.08"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.4" expl="correctness of parameter gcd" sum="1221b85597e3a6d4bbdb929662515a1b" proved="true" expanded="true">
<goal name="WP_parameter gcd.2.4" expl="correctness of parameter gcd" sum="dd3ce062113c8bf7e99d5842826cbef3" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter gcd.2.5" expl="correctness of parameter gcd" sum="dd8408987193bff8e40272015be1aa9d" proved="true" expanded="true">
<goal name="WP_parameter gcd.2.5" expl="correctness of parameter gcd" sum="393a23c2dbe93d5227c05add6207598a" proved="true" expanded="true">
<proof prover="cvc3" timelimit="3" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter gcd.3" expl="loop variant decreases" sum="cca2a902409976d7fe1249041e32fc6e" proved="true" expanded="true">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<goal name="WP_parameter gcd.3" expl="loop variant decreases" sum="365b0eb4709478b597d2122a5c3c67c1" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.09"/>
<result status="valid" time="0.06"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter gcd.4" expl="normal postcondition" sum="70282398b1f17ace6b7f8ea5e5755ba1" proved="true" expanded="true">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter gcd.4" expl="normal postcondition" sum="b99571221c54c860bd5407d585fc8cdd" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="1.14"/>
<result status="valid" time="0.49"/>
</proof>
</goal>
</transf>
......
examples/programs/isqrt/why3session.xml
View file @ aee107f3
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/isqrt/why3session.xml">
<why3session name="examples/programs/isqrt/why3session.xml">
<file name="../isqrt.mlw" verified="true" expanded="true">
<theory name="M" verified="true" expanded="true">
<goal name="WP_parameter isqrt" expl="correctness of parameter isqrt" sum="510de4257915daa3e680ba4e3c8515f1" proved="true" expanded="true">
<goal name="WP_parameter isqrt" expl="correctness of parameter isqrt" sum="5c9a0a28616c8a34d7fb4e3e77a12070" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.12"/>
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter main" expl="correctness of parameter main" sum="fad1c189aa702c8c6c682810d5ecf636" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.11"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<goal name="WP_parameter main" expl="correctness of parameter main" sum="7960ecfe2bbd563711f4786261fcb516" proved="true" expanded="true">
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
examples/programs/list_rev/why3session.xml
View file @ aee107f3
......@@ -3,67 +3,67 @@
<why3session name="examples/programs/list_rev/why3session.xml">
<file name="../list_rev.mlw" verified="false" expanded="true">
<theory name="M" verified="false" expanded="true">
<goal name="acyclic_list" sum="14b23a72bdf3ddafa531460f9838d56d" proved="false" expanded="true">
<goal name="acyclic_list" sum="05ff1ad20f5af90fc986f7d1deb8acbf" proved="false" expanded="true">
</goal>
<goal name="consistent" sum="373d5b25560c53e2797b67419b7ff691" proved="false" expanded="true">
<goal name="consistent" sum="678d57b4a5464ed1788c9284cd3deb14" proved="false" expanded="true">
</goal>
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="b33dc5e7178219ce350fce83005647ef" proved="true" expanded="true">
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="1ed3408e037f1f79e9735208d22637d9" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal name="reverse_append" sum="1533f78841b3afe619b329869e8d0af6" proved="false" expanded="true">
<goal name="reverse_append" sum="95eaedbd88c6733c31f6f90543952407" proved="false" expanded="true">
</goal>
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="e19607dfb73eba248a0c06d25548625d" proved="false" expanded="true">
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="4087cd4ed78b8c5468550eec66d4564d" proved="false" expanded="true">
</goal>
</theory>
<theory name="M2" verified="false" expanded="true">
<goal name="is_list_disjoint_case" sum="1babcc38937f94867ddd31ce304b7e74" proved="true" expanded="true">
<goal name="is_list_disjoint_case" sum="db8d14254ea7d12f7f7bbb446ee006eb" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="frame_list" sum="6832b0f09ea49b1a68df28ae5d8cc5ba" proved="true" expanded="true">
<goal name="frame_list" sum="bb671f60ef471cba398e52a876544a54" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_list_1.v" obsolete="false">
<result status="valid" time="0.72"/>
<result status="valid" time="0.50"/>
</proof>
</goal>
<goal name="frame_list_ft" sum="60296b3f03b1fc700582f4a9e9d6b98b" proved="true" expanded="true">
<goal name="frame_list_ft" sum="d0c0dd407e6667c967cd37f14169af5e" proved="false" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_list_ft_1.v" obsolete="false">
<result status="valid" time="0.74"/>
<result status="unknown" time="0.48"/>
</proof>
</goal>
<goal name="acyclic_list" sum="c621805c935ee753897c237a73f10bad" proved="false" expanded="true">
<goal name="acyclic_list" sum="9beb2427d92c0d05c7ab34738d84fb20" proved="false" expanded="true">
</goal>
<goal name="consistent" sum="08a4374f096f4d7cd99f4f52fc96b3f7" proved="false" expanded="true">
<goal name="consistent" sum="c4812a324be896e9f0a42c752b48a304" proved="false" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.04"/>
<result status="unknown" time="0.03"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.25"/>
<result status="timeout" time="10.11"/>
</proof>
</goal>
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="b0d03c98bb5c3e11156af8522cbb9b03" proved="true" expanded="true">
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="2cf5c0afcc43f0a5bf2667c7c738c555" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="frame_model" sum="9953603df5d42e7cae815cbc5613db81" proved="true" expanded="true">
<goal name="frame_model" sum="d5fd36bbd6e0e2aebeea5703bbf7b4d7" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_model_1.v" obsolete="false">
<result status="valid" time="0.75"/>
<result status="valid" time="0.53"/>
</proof>
</goal>
<goal name="consistent_behv" sum="67bef8b4f715a36d1daec8ca46e4d812" proved="false" expanded="true">
<goal name="consistent_behv" sum="f9e3c4ba36897ccd68e9407e528ff384" proved="false" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.84"/>
<result status="timeout" time="10.04"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.56"/>
<result status="timeout" time="10.05"/>
</proof>
</goal>
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="3177c7272f5a46808daf16bb3365415c" proved="true" expanded="true">
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="52a60a766a87079ec4ccbf52ed6012eb" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.20"/>
<result status="valid" time="0.18"/>
</proof>
</goal>
</theory>
......
examples/programs/mac_carthy/why3session.xml
View file @ aee107f3
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/mac_carthy/why3session.xml">
<why3session name="examples/programs/mac_carthy/why3session.xml">
<file name="../mac_carthy.mlw" verified="true" expanded="true">
<theory name="M" verified="true" expanded="true">
<goal name="WP_parameter f91" expl="correctness of parameter f91" sum="d76ec4e4b18463778c1d69a5f339cd5b" proved="true" expanded="true">
<goal name="WP_parameter f91" expl="correctness of parameter f91" sum="7abacd70509916020a75c246a162149a" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter f91_nonrec" expl="correctness of parameter f91_nonrec" sum="0a7c396695b0240cd521dde6e0557c36" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
<goal name="WP_parameter f91_nonrec" expl="correctness of parameter f91_nonrec" sum="dd51d83389d374c543e554d535df25d2" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="1.46"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.52"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
......
examples/programs/my_cosine/why3session.xml
View file @ aee107f3
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/my_cosine/why3session.xml">
<file name="../my_cosine.mlw" verified="true" expanded="true">
<theory name="M" verified="true" expanded="true">
<goal name="WP_parameter my_cosine" expl="correctness of parameter my_cosine" sum="986f977f7129151df7340d17164762c3" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="assertion" sum="42f9206597da619fa67e4871bf991914" proved="true" expanded="true">
<file name="../my_cosine.mlw" verified="false" expanded="true">
<theory name="M" verified="false" expanded="true">
<goal name="WP_parameter my_cosine" expl="correctness of parameter my_cosine" sum="f89fdf11644955925594e36ac13fca80" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="assertion" sum="e5882e289db8c6ba752b0197911cfa23" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="my_cosine.mlw_M_WP_parameter my_cosine_1.v" obsolete="false">
<result status="valid" time="3.82"/>
<result status="valid" time="3.63"/>
</proof>
</goal>
<goal name="WP_parameter my_cosine.2" expl="precondition" sum="be0701645667327c36cf66484840bf90" proved="true" expanded="true">
<goal name="WP_parameter my_cosine.2" expl="precondition" sum="835240929a7ed987a4162d95e5c84f6a" proved="true" expanded="true">
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter my_cosine.3" expl="precondition" sum="3ad91864f24b8a31a628b48823b41ea2" proved="true" expanded="true">
<goal name="WP_parameter my_cosine.3" expl="precondition" sum="e76b668f84980d8e838e3a29329b0078" proved="true" expanded="true">
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter my_cosine.4" expl="precondition" sum="6a3e5463b9408c699f0550a24603937a" proved="true" expanded="true">
<goal name="WP_parameter my_cosine.4" expl="precondition" sum="4a7ffc5f36f6cb1ee98787dec2d021cb" proved="true" expanded="true">
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter my_cosine.5" expl="normal postcondition" sum="9148268517dc60d188ee0ee3565f9253" proved="true" expanded="true">
<goal name="WP_parameter my_cosine.5" expl="normal postcondition" sum="ede46e25abe361f5d69fd104ad839c4c" proved="false" expanded="true">
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="unknown" time="0.00"/>
</proof>
</goal>
</transf>
......
examples/programs/power.mlw
View file @ aee107f3
......@@ -17,6 +17,9 @@ theory Power
lemma Power_mult : forall x n m : int. 0 <= n -> 0 <= m ->
power x (n * m) = power (power x n) m
lemma Power_mult2 : forall x y n : int. 0 <= n ->
power (x * y) n = power x n * power y n
end
module M
......
examples/programs/power/power.mlw_Power_Power_mult2_1.v 0 → 100644
View file @ aee107f3
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
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 power: Z -> Z -> Z.
Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
Axiom Power_s : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x
n) = (x * (power x (n - 1%Z)%Z))%Z).
Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
Axiom Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
Axiom Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n * m)%Z) = (power (power x n) m))).
Theorem Power_mult2 : forall (x:Z) (y:Z) (n:Z), (0%Z <= n)%Z ->
((power (x * y)%Z n) = ((power x n) * (power y n))%Z).
(* YOU MAY EDIT THE PROOF BELOW *)
intros x y n Hn.
generalize Hn.
pattern n.
apply natlike_ind; auto.
intros; do 3 rewrite Power_0.
omega.
intros.
rewrite Power_s.
2:omega.
rewrite (Power_s x (Zsucc x0)).
rewrite (Power_s y (Zsucc x0)).
replace (Zsucc x0 - 1)%Z with x0 by omega.
rewrite H0.
ring.
omega.
omega.
omega.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/power/why3session.xml
View file @ aee107f3
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/power/why3session.xml">
<file name="../power.mlw" verified="false" expanded="true">
<theory name="Power" verified="true" expanded="false">
<goal name="Power_1" sum="1db7c130e0faaa3525077846831aadf3" proved="true" expanded="false">
<file name="../power.mlw" verified="true" expanded="true">
<theory name="Power" verified="true" expanded="true">
<goal name="Power_1" sum="1db7c130e0faaa3525077846831aadf3" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......@@ -14,69 +14,65 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="true" expanded="false">
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="power.mlw_Power_Power_sum_1.v" obsolete="false">
<result status="valid" time="0.46"/>
</proof>
</goal>
<goal name="Power_mult" sum="9d09d633adb75294ad19c24d7ad24bf4" proved="true" expanded="false">
<goal name="Power_mult" sum="9d09d633adb75294ad19c24d7ad24bf4" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="power.mlw_Power_Power_mult_1.v" obsolete="false">
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal name="Power_mult2" sum="c37356cfaed29d43e8813ffc76d4ea37" proved="true" expanded="true">
<proof prover="coq" timelimit="5" edited="power.mlw_Power_Power_mult2_1.v" obsolete="false">
<result status="valid" time="0.52"/>
</proof>
</goal>
</theory>
<theory name="M" verified="false" expanded="true">
<goal name="WP_parameter fast_exp" expl="correctness of parameter fast_exp" sum="ff0a5f4d7ce2252d7f09664075c560a8" proved="true" expanded="false">
<theory name="M" verified="true" expanded="true">
<goal name="WP_parameter fast_exp" expl="correctness of parameter fast_exp" sum="ada75a97b847f6c89f173745c047f4f6" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative" expl="correctness of parameter fast_exp_imperative" sum="22f72b816b6021c98b7d03397cb1d7fd" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter fast_exp_imperative.1" expl="loop invariant init" sum="0bac504113a8f4e466cd5612d00220fa" proved="true" expanded="false">
<goal name="WP_parameter fast_exp_imperative" expl="correctness of parameter fast_exp_imperative" sum="e63feaa4075e2c29b1d2e508ef9a86bc" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter fast_exp_imperative.1" expl="loop invariant init" sum="f0a22ad175a48b43773b37c4a2565beb" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.2" expl="loop invariant preservation" sum="5117e72c11ee204306335e1da3b9a5e7" proved="true" expanded="false">
<goal name="WP_parameter fast_exp_imperative.2" expl="loop invariant preservation" sum="d268dda056e1d709305e69a650f8bcba" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.3" expl="loop variant decreases" sum="80be8265c76399ff1ed013b560c05ac9" proved="true" expanded="false">
<goal name="WP_parameter fast_exp_imperative.3" expl="loop variant decreases" sum="b283152678ce6a261050e574e7fb72b1" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4" expl="loop invariant preservation" sum="0c03c29f50e52bd5961ca54bd12cf4b9" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter fast_exp_imperative.4.1" expl="correctness of parameter fast_exp_imperative" sum="7ab6e51299cce66c2e5f2754452a91db" proved="true" expanded="true">
<goal name="WP_parameter fast_exp_imperative.4" expl="loop invariant preservation" sum="e6449071b108723a7787ee383b863dd4" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter fast_exp_imperative.4.1" expl="correctness of parameter fast_exp_imperative" sum="1d0c559d1a4eb1cfe9233489abfef5c8" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4.2" expl="correctness of parameter fast_exp_imperative" sum="153686c76ecf6d6a9fa404474076db03" proved="false" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="7.32"/>