cleaning up proofs

parent 988d64dc
......@@ -26,8 +26,7 @@ module Quicksort
if l < r then begin
let v = t[l] in
let m = ref l in
'L: begin
for i = l + 1 to r do
'L: for i = l + 1 to r do
invariant { (forall j:int. l < j <= !m -> t[j] < v) /\
(forall j:int. !m < j < i -> t[j] >= v) /\
permut_sub t (at t 'L) l (r+1) /\
......@@ -37,7 +36,7 @@ module Quicksort
swap t l !m;
quick_rec t l (!m - 1);
quick_rec t (!m + 1) r
end end
end
{ sorted_sub t l (r+1) /\ permut_sub t (old t) l (r+1) }
let quicksort (t : array int) =
......
......@@ -12,12 +12,12 @@
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter quick_rec.1" expl="precondition" sum="afb020494e403a393ab8e90f692bc69b" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.2" expl="precondition" sum="a3181f1907824ed087e006f87be7bd9e" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.3" expl="precondition" sum="8edc81919941af864219896fecd0637b" proved="true" expanded="false">
......@@ -35,7 +35,7 @@
</goal>
<goal name="WP_parameter quick_rec.5" expl="normal postcondition" sum="baa25029fb0a71d8acaf5f993d04baff" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<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">
......@@ -44,16 +44,16 @@
</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="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="true">
<result status="timeout" time="10.13"/>
</proof>
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<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">
......@@ -63,7 +63,7 @@
</goal>
<goal name="WP_parameter quick_rec.7.3" expl="for loop preservation" sum="228d233acd3a7e42d2e375f8e798d716" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
<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">
......@@ -73,32 +73,32 @@
</goal>
<goal name="WP_parameter quick_rec.7.5" expl="for loop preservation" sum="26d5fa5d233855efc8b3da64ecea09d1" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.39"/>
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<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">
......@@ -108,24 +108,24 @@
</goal>
<goal name="WP_parameter quick_rec.7.12" expl="for loop preservation" sum="bbf98e9044079713e7ab2698e11485bd" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<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">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.9" expl="precondition" sum="64b33af689e246d177effa0b1855ce6c" proved="true" expanded="false">
......@@ -137,12 +137,12 @@
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<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">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<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">
......@@ -164,7 +164,7 @@
</goal>
<goal name="WP_parameter quick_rec.12" expl="normal postcondition" sum="34d47e5d2d59419520785959c4866c68" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
......@@ -178,13 +178,13 @@
</goal>
<goal name="WP_parameter quicksort.2" expl="normal postcondition" sum="e3ed7aa7c2a41c52acb920e4e3a3d9f0" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
</goal>
</transf>
......
(* Selectino sort. *)
(* Selection sort. *)
module Quicksort
module SelectionSort
use import int.Int
use import module ref.Ref
......
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