Commit bfc08a83 authored by Andrei Paskevich's avatar Andrei Paskevich

update a couple of sessions

parent cb07f364
......@@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../add_list.mlw" expanded="true">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="AddListRec" sum="f1b4c4e0923c97bb07f0497e41cca3dd" expanded="true">
<theory name="AddListRec" sum="a7bc617783ac097fd03baf5114e10fca" expanded="true">
<goal name="VC sum" expl="VC for sum">
<transf name="split_goal_wp">
<goal name="VC sum.1" expl="1. postcondition">
......@@ -35,7 +35,7 @@
</transf>
</goal>
</theory>
<theory name="AddListImp" sum="e8c88c18c52faab3c58cf2482eb150fd" expanded="true">
<theory name="AddListImp" sum="b59d5583deafd1e0a51ec8df39195de2" expanded="true">
<goal name="VC sum" expl="VC for sum">
<transf name="split_goal_wp">
<goal name="VC sum.1" expl="1. loop invariant init">
......
......@@ -6,7 +6,7 @@
<prover id="5" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../algo63.mlw" expanded="true">
<theory name="Algo63" sum="0cef588c003de6fc6479fa321d82c36a" expanded="true">
<theory name="Algo63" sum="4c5e496d63dc8e8c27cfd2ce83c3b7fc" expanded="true">
<goal name="VC exchange" expl="VC for exchange">
<transf name="split_goal_wp">
<goal name="VC exchange.1" expl="1. index in array bounds">
......@@ -88,11 +88,11 @@
<proof prover="4"><result status="valid" time="0.05" steps="128"/></proof>
</goal>
<goal name="VC partition_.18" expl="18. precondition">
<proof prover="4"><result status="valid" time="1.37" steps="666"/></proof>
<proof prover="4"><result status="valid" time="2.44" steps="780"/></proof>
</goal>
<goal name="VC partition_.19" expl="19. precondition">
<proof prover="4" obsolete="true"><result status="timeout" time="5.01"/></proof>
<proof prover="5" obsolete="true"><result status="timeout" time="5.04"/></proof>
<proof prover="4"><result status="timeout" time="5.01"/></proof>
<proof prover="5"><result status="timeout" time="5.04"/></proof>
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC partition_.20" expl="20. precondition">
......@@ -168,15 +168,15 @@
<proof prover="4"><result status="valid" time="0.08" steps="127"/></proof>
</goal>
<goal name="VC partition_.44" expl="44. postcondition">
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC partition_.45" expl="45. postcondition">
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC partition_.46" expl="46. postcondition">
<proof prover="4"><result status="valid" time="4.52" steps="1968"/></proof>
<proof prover="4"><result status="valid" time="5.75" steps="1961"/></proof>
</goal>
<goal name="VC partition_.47" expl="47. precondition">
<proof prover="4"><result status="valid" time="0.02" steps="19"/></proof>
......@@ -188,14 +188,14 @@
<proof prover="4"><result status="valid" time="0.05" steps="128"/></proof>
</goal>
<goal name="VC partition_.50" expl="50. postcondition">
<proof prover="4"><result status="valid" time="2.03" steps="1129"/></proof>
<proof prover="4"><result status="valid" time="3.15" steps="1129"/></proof>
</goal>
<goal name="VC partition_.51" expl="51. postcondition">
<proof prover="4" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC partition_.52" expl="52. postcondition">
<proof prover="4"><result status="valid" time="0.49" steps="328"/></proof>
<proof prover="4"><result status="valid" time="0.65" steps="328"/></proof>
</goal>
<goal name="VC partition_.53" expl="53. postcondition">
<proof prover="4"><result status="valid" time="0.02" steps="18"/></proof>
......
......@@ -2,9 +2,9 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="6" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="1" memlimit="1000"/>
<file name="../algo64.mlw">
<theory name="Algo64" sum="21130e5024a2be148a1c22eaa59415a8">
<theory name="Algo64" sum="2b1c30c3b4ab9d2ffbed6f1f7be4c3ae">
<goal name="VC quicksort" expl="VC for quicksort">
<transf name="split_goal_wp">
<goal name="VC quicksort.1" expl="1. precondition">
......
......@@ -4,9 +4,9 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="1" memlimit="1000"/>
<file name="../algo65.mlw" expanded="true">
<theory name="Algo65" sum="9534961d2656c4644acd5f2173995f2a" expanded="true">
<theory name="Algo65" sum="c83da6bd17073218a1df71dece43efcb" expanded="true">
<goal name="VC find" expl="VC for find" expanded="true">
<proof prover="0"><result status="valid" time="4.01" steps="6656"/></proof>
<proof prover="0"><result status="valid" time="4.01" steps="6546"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,38 +2,43 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true">
<theory name="AllDistinct" sum="a41b03c7310badbe67937c261148930c" expanded="true">
<theory name="AllDistinct" sum="d0fdc968e71fba542b0c675b6cab2360" expanded="true">
<goal name="VC all_distinct" expl="VC for all_distinct" expanded="true">
<proof prover="0"><result status="valid" time="0.09" steps="244"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="VC all_distinct.1" expl="1. array creation size">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC all_distinct.2" expl="2. loop invariant init">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
<goal name="VC all_distinct.2" expl="2. postcondition">
<proof prover="0" steplimit="-1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC all_distinct.3" expl="3. loop invariant init">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC all_distinct.4" expl="4. index in array bounds">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
<goal name="VC all_distinct.4" expl="4. loop invariant init">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC all_distinct.5" expl="5. index in array bounds">
<proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC all_distinct.6" expl="6. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC all_distinct.7" expl="7. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC all_distinct.8" expl="8. index in array bounds">
<proof prover="0"><result status="valid" time="0.00" steps="19"/></proof>
</goal>
<goal name="VC all_distinct.7" expl="7. loop invariant preservation">
<goal name="VC all_distinct.9" expl="9. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="53"/></proof>
</goal>
<goal name="VC all_distinct.8" expl="8. loop invariant preservation">
<goal name="VC all_distinct.10" expl="10. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="55"/></proof>
</goal>
<goal name="VC all_distinct.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="42"/></proof>
<goal name="VC all_distinct.11" expl="11. postcondition">
<proof prover="0" steplimit="-1"><result status="valid" time="0.00" steps="18"/></proof>
</goal>
</transf>
</goal>
......
......@@ -2,69 +2,21 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="1000"/>
<file name="../arm.mlw" expanded="true">
<theory name="M" sum="0d719c3e6262bb28f7a388d2aa2d5410" expanded="true">
<goal name="WP_parameter insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal_wp">
<goal name="WP_parameter insertion_sort.1" expl="1. loop invariant init">
<proof prover="3" memlimit="1000"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.2" expl="2. loop invariant init">
<proof prover="3" memlimit="1000"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.3" expl="3. type invariant">
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.4" expl="4. index in array bounds">
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.5" expl="5. index in array bounds">
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.6" expl="6. index in array bounds">
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.7" expl="7. index in array bounds">
<proof prover="3" memlimit="1000"><result status="valid" time="0.03" steps="21"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.8" expl="8. index in array bounds">
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.9" expl="9. index in array bounds">
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.10" expl="10. loop invariant preservation">
<proof prover="3" memlimit="1000"><result status="valid" time="1.17" steps="75"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.11" expl="11. loop variant decrease">
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.12" expl="12. loop invariant preservation">
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.13" expl="13. loop variant decrease">
<proof prover="3" memlimit="1000"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.14" expl="14. type invariant">
<proof prover="3" memlimit="1000"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter insertion_sort.15" expl="15. postcondition">
<proof prover="3" memlimit="1000"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
<theory name="M" sum="517e5ea7dffd768f289bfb648bd8700b" expanded="true">
<goal name="VC insertion_sort" expl="VC for insertion_sort" expanded="true">
<proof prover="0"><result status="valid" time="0.06" steps="94"/></proof>
</goal>
</theory>
<theory name="ARM" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="InsertionSortExample" sum="8f826701fa05e53c78b726425a76d7d8" expanded="true">
<goal name="WP_parameter path_init_l2" expl="VC for path_init_l2">
<proof prover="1"><result status="valid" time="0.14"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.02" steps="17"/></proof>
<theory name="InsertionSortExample" sum="8a3d58ebfc4e621c805950d96e63138f" expanded="true">
<goal name="VC path_init_l2" expl="VC for path_init_l2" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter path_l2_exit" expl="VC for path_l2_exit">
<proof prover="3" timelimit="10"><result status="valid" time="0.01" steps="10"/></proof>
<goal name="VC path_l2_exit" expl="VC for path_l2_exit" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,17 +2,16 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="10" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="1000"/>
<file name="../assigning_meanings_to_programs.mlw">
<theory name="Sum" sum="606dc92ebecb74d906410b581994896f" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="2"><result status="valid" time="0.02" steps="21"/></proof>
<theory name="Sum" sum="abdbe8856020a569779b03c31d21b892">
<goal name="VC sum" expl="VC for sum">
<proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
</theory>
<theory name="Division" sum="67dbd39ccfe310fac83f690ec134b490" expanded="true">
<goal name="WP_parameter division" expl="VC for division" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<theory name="Division" sum="fd661d5fb80f80ed298bacb077c88a90">
<goal name="VC division" expl="VC for division">
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
</theory>
</file>
......
......@@ -11,23 +11,19 @@ module BubbleSort
use import array.ArrayPermut
use import array.ArrayEq
let bubble_sort (a: array int)
ensures { permut_all (old a) a }
ensures { sorted a }
= label Init in
for i = length a - 1 downto 1 do
invariant { permut_all (a at Init) a }
= for i = length a - 1 downto 1 do
invariant { permut_all (old a) a }
invariant { sorted_sub a i (length a) }
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
}
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] }
for j = 0 to i - 1 do
invariant { permut_all (a at Init) a }
invariant { permut_all (old a) a }
invariant { sorted_sub a i (length a) }
invariant { forall k1 k2: int.
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2]
}
0 <= k1 <= i < k2 < length a -> a[k1] <= a[k2] }
invariant { forall k. 0 <= k <= j -> a[k] <= a[j] }
if a[j] > a[j+1] then swap a j (j+1);
done;
......
......@@ -2,9 +2,9 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="1" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="1" memlimit="1000"/>
<file name="../bubble_sort.mlw" expanded="true">
<theory name="BubbleSort" sum="e8e176a63dc9cbea2dbc1372aae5c5ba" expanded="true">
<theory name="BubbleSort" sum="3fb187c833b7f1d23b94d72c6bdacd3c" expanded="true">
<goal name="VC bubble_sort" expl="VC for bubble_sort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC bubble_sort.1" expl="1. postcondition">
......
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