cleaning up proofs

parent 85f63936
......@@ -3,14 +3,14 @@
<why3session name="examples/programs/quicksort/why3session.xml">
<file name="../quicksort.mlw" verified="true" expanded="true">
<theory name="WP Quicksort" verified="true" expanded="true">
<goal name="WP_parameter swap" expl="correctness of parameter swap" sum="41390d74df59a170f969e943142ebb7b" proved="true" expanded="false">
<goal name="WP_parameter swap" expl="correctness of parameter swap" sum="41390d74df59a170f969e943142ebb7b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec" expl="correctness of parameter quick_rec" sum="429418ca6a20864d185b961d43f30d8f" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter quick_rec.1" expl="precondition" sum="afb020494e403a393ab8e90f692bc69b" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.1" expl="precondition" sum="afb020494e403a393ab8e90f692bc69b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
......@@ -20,137 +20,128 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.3" expl="precondition" sum="8edc81919941af864219896fecd0637b" proved="true" expanded="false">
<proof prover="coq" timelimit="10" edited="quicksort_WP_Quicksort_WP_parameter_quick_rec_1.v" obsolete="true"><undone/>
</proof>
<goal name="WP_parameter quick_rec.3" expl="precondition" sum="8edc81919941af864219896fecd0637b" 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 quick_rec.4" expl="precondition" sum="fb0adf4bd54b37761c3cde3fe39f670e" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.4" expl="precondition" sum="fb0adf4bd54b37761c3cde3fe39f670e" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.5" expl="normal postcondition" sum="baa25029fb0a71d8acaf5f993d04baff" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.5" expl="normal postcondition" sum="baa25029fb0a71d8acaf5f993d04baff" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.6" expl="for loop initialization" sum="1c4177f71f9cbbbbbfd4115780641e1c" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.6" expl="for loop initialization" sum="1c4177f71f9cbbbbbfd4115780641e1c" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.7" expl="for loop preservation" sum="889feaae94e94c3d8f72805ff307f9e9" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="true">
<result status="timeout" time="10.13"/>
</proof>
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="timeout" time="10.03"/>
</proof>
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.1" expl="for loop preservation" sum="9c0efe9ed6146211b6f0e90c55ea1c4a" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7" expl="for loop preservation" sum="889feaae94e94c3d8f72805ff307f9e9" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter quick_rec.7.1" expl="for loop preservation" sum="9c0efe9ed6146211b6f0e90c55ea1c4a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.7.2" expl="for loop preservation" sum="15a8b476dd7c6f8af9213b9b00a54641" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.2" expl="for loop preservation" sum="15a8b476dd7c6f8af9213b9b00a54641" 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 quick_rec.7.3" expl="for loop preservation" sum="228d233acd3a7e42d2e375f8e798d716" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.3" expl="for loop preservation" sum="228d233acd3a7e42d2e375f8e798d716" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.7.4" expl="for loop preservation" sum="87f84d18958588ba63f323710cd9d25a" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.4" expl="for loop preservation" sum="87f84d18958588ba63f323710cd9d25a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.7.5" expl="for loop preservation" sum="26d5fa5d233855efc8b3da64ecea09d1" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.5" expl="for loop preservation" sum="26d5fa5d233855efc8b3da64ecea09d1" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.38"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.7.6" expl="for loop preservation" sum="1e708347df6438df8c3fa3628f6ebdec" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.6" expl="for loop preservation" sum="1e708347df6438df8c3fa3628f6ebdec" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.7.7" expl="for loop preservation" sum="c1cae61d1f69fc8fb8ea60c2d075a36d" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.7" expl="for loop preservation" sum="c1cae61d1f69fc8fb8ea60c2d075a36d" 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 quick_rec.7.8" expl="for loop preservation" sum="524f8413f2d8a9de2bd6a6ad2c4a088e" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.8" expl="for loop preservation" sum="524f8413f2d8a9de2bd6a6ad2c4a088e" 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 quick_rec.7.9" expl="for loop preservation" sum="0b64cd1805d7a57e8bff8751f2baf675" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.9" expl="for loop preservation" sum="0b64cd1805d7a57e8bff8751f2baf675" 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 quick_rec.7.10" expl="for loop preservation" sum="497463ab5695da47ad41c0201d93fbb4" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.10" expl="for loop preservation" sum="497463ab5695da47ad41c0201d93fbb4" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.7.11" expl="for loop preservation" sum="2e8721d1670e2d8ec7740d91c87a9e61" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.11" expl="for loop preservation" sum="2e8721d1670e2d8ec7740d91c87a9e61" 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 quick_rec.7.12" expl="for loop preservation" sum="bbf98e9044079713e7ab2698e11485bd" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.12" expl="for loop preservation" sum="bbf98e9044079713e7ab2698e11485bd" 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 quick_rec.7.13" expl="for loop preservation" sum="72626c63afff611555f9e512efa1f1fc" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.13" expl="for loop preservation" sum="72626c63afff611555f9e512efa1f1fc" 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 quick_rec.7.14" expl="for loop preservation" sum="d5eb94ee88f2a6582d26d227213096b3" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.7.14" expl="for loop preservation" sum="d5eb94ee88f2a6582d26d227213096b3" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter quick_rec.8" expl="precondition" sum="33039b31c9c6180ab52eaf5492f2bc01" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.8" expl="precondition" sum="33039b31c9c6180ab52eaf5492f2bc01" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.9" expl="precondition" sum="64b33af689e246d177effa0b1855ce6c" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.9" expl="precondition" sum="64b33af689e246d177effa0b1855ce6c" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.10" expl="precondition" sum="ff22ded78eff20d1cfa55d773763a9d5" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.10.1" expl="correctness of parameter quick_rec" sum="377daa4ea73659b14aa5f353a807b1cb" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.10" expl="precondition" sum="ff22ded78eff20d1cfa55d773763a9d5" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter quick_rec.10.1" expl="correctness of parameter quick_rec" sum="377daa4ea73659b14aa5f353a807b1cb" 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 quick_rec.10.2" expl="correctness of parameter quick_rec" sum="89ea54e07fd5f22cfcb869807c6ccb81" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.10.2" expl="correctness of parameter quick_rec" sum="89ea54e07fd5f22cfcb869807c6ccb81" 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 quick_rec.10.3" expl="correctness of parameter quick_rec" sum="ce9047573188eebeffdf2a00a09c300c" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.10.3" expl="correctness of parameter quick_rec" sum="ce9047573188eebeffdf2a00a09c300c" 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 quick_rec.10.4" expl="correctness of parameter quick_rec" sum="c13522eaa1a26354dd7afb46681cc4e8" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.10.4" expl="correctness of parameter quick_rec" sum="c13522eaa1a26354dd7afb46681cc4e8" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
......@@ -162,21 +153,21 @@
<result status="valid" time="2.27"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.12" expl="normal postcondition" sum="34d47e5d2d59419520785959c4866c68" proved="true" expanded="false">
<goal name="WP_parameter quick_rec.12" expl="normal postcondition" sum="34d47e5d2d59419520785959c4866c68" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter quicksort" expl="correctness of parameter quicksort" sum="f4bb2417ab497ffde7f96bb0a1dd4587" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter quicksort.1" expl="precondition" sum="4da62dee020a36946666099e79806868" proved="true" expanded="false">
<goal name="WP_parameter quicksort" expl="correctness of parameter quicksort" sum="f4bb2417ab497ffde7f96bb0a1dd4587" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter quicksort.1" expl="precondition" sum="4da62dee020a36946666099e79806868" 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 quicksort.2" expl="normal postcondition" sum="e3ed7aa7c2a41c52acb920e4e3a3d9f0" proved="true" expanded="false">
<goal name="WP_parameter quicksort.2" expl="normal postcondition" sum="e3ed7aa7c2a41c52acb920e4e3a3d9f0" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
......
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