updated proof sesssions

parent 63b8f6d0
...@@ -40,7 +40,6 @@ generate_all_trees.mlw ...@@ -40,7 +40,6 @@ generate_all_trees.mlw
hackers-delight.mlw hackers-delight.mlw
hashtbl_impl.mlw hashtbl_impl.mlw
ieee_float.mlw ieee_float.mlw
isqrt.mlw
kmp.mlw kmp.mlw
knuth_prime_numbers.mlw knuth_prime_numbers.mlw
koda_ruskey.mlw koda_ruskey.mlw
...@@ -48,7 +47,6 @@ lcp.mlw ...@@ -48,7 +47,6 @@ lcp.mlw
linear_probing.mlw linear_probing.mlw
linked_list_rev.mlw linked_list_rev.mlw
maximum_subarray.mlw maximum_subarray.mlw
max_matrix.mlw
mergesort_list.mlw mergesort_list.mlw
my_cosine.mlw my_cosine.mlw
optimal_replay.mlw optimal_replay.mlw
...@@ -56,10 +54,8 @@ pairing_heap_bin.mlw ...@@ -56,10 +54,8 @@ pairing_heap_bin.mlw
pairing_heap.mlw pairing_heap.mlw
patience.mlw patience.mlw
pigeonhole.mlw pigeonhole.mlw
power.mlw
queens_bv.mlw queens_bv.mlw
queens.mlw queens.mlw
quicksort.mlw
random_access_list.mlw random_access_list.mlw
register_allocation.mlw register_allocation.mlw
relabel.mlw relabel.mlw
...@@ -67,14 +63,12 @@ residual.mlw ...@@ -67,14 +63,12 @@ residual.mlw
rightmostbittrick.mlw rightmostbittrick.mlw
schorr_waite.mlw schorr_waite.mlw
schorr_waite_via_recursion.mlw schorr_waite_via_recursion.mlw
selection_sort.mlw
sieve.mlw sieve.mlw
skew_heaps.mlw skew_heaps.mlw
snapshotable_trees.mlw snapshotable_trees.mlw
sorted_list.mlw sorted_list.mlw
sudoku.mlw sudoku.mlw
sum_of_digits.mlw sum_of_digits.mlw
swap.mlw
there_and_back_again.mlw there_and_back_again.mlw
topological_sorting.mlw topological_sorting.mlw
tortoise_and_hare.mlw tortoise_and_hare.mlw
......
This diff is collapsed.
...@@ -60,8 +60,7 @@ ...@@ -60,8 +60,7 @@
</goal> </goal>
<goal name="VC sqrt.11" expl="11. assertion" expanded="true"> <goal name="VC sqrt.11" expl="11. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="VC sqrt.11.1" expl="1. VC for sqrt"> <goal name="VC sqrt.11.1" expl="1. VC for sqrt" expanded="true">
<proof prover="2"><undone/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof> <proof prover="7"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC sqrt.11.2" expl="2. VC for sqrt"> <goal name="VC sqrt.11.2" expl="2. VC for sqrt">
......
...@@ -2,137 +2,70 @@ ...@@ -2,137 +2,70 @@
<!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="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="30" steplimit="0" memlimit="1000"/> <prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="5" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../max_matrix.mlw" expanded="true"> <file name="../max_matrix.mlw" expanded="true">
<theory name="Bitset" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="Bitset" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="HashTable" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="HashTable" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="MaxMatrixMemo" sum="60d6a7dda5b713ca659b3a4deef37b09" expanded="true"> <theory name="MaxMatrixMemo" sum="fcec2dfa63ba5bba88e2303600274724" expanded="true">
<goal name="VC n" expl="VC for n" expanded="true">
<proof prover="3"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC m" expl="VC for m" expanded="true">
<proof prover="3"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="sum_ind"> <goal name="sum_ind">
<proof prover="4" timelimit="47" memlimit="0"><result status="valid" time="0.15" steps="45"/></proof> <proof prover="3"><result status="valid" time="0.03" steps="65"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum" expl="VC for maximum" expanded="true"> <goal name="VC maximum" expl="VC for maximum" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter maximum.1" expl="1. postcondition"> <goal name="VC maximum.1" expl="1. postcondition">
<proof prover="4"><result status="valid" time="0.02" steps="38"/></proof> <proof prover="3"><result status="valid" time="0.01" steps="45"/></proof>
</goal>
<goal name="WP_parameter maximum.2" expl="2. assertion">
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum.3" expl="3. postcondition"> <goal name="VC maximum.2" expl="2. loop bounds">
<proof prover="4"><result status="valid" time="0.01" steps="6"/></proof> <proof prover="3"><result status="valid" time="0.00" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum.4" expl="4. loop invariant init"> <goal name="VC maximum.3" expl="3. loop invariant init">
<proof prover="4"><result status="valid" time="0.00" steps="8"/></proof> <proof prover="3"><result status="valid" time="0.00" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum.5" expl="5. variant decrease"> <goal name="VC maximum.4" expl="4. variant decrease">
<proof prover="4"><result status="valid" time="0.02" steps="13"/></proof> <proof prover="3"><result status="valid" time="0.00" steps="14"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum.6" expl="6. precondition"> <goal name="VC maximum.5" expl="5. precondition">
<proof prover="4"><result status="valid" time="0.03" steps="36"/></proof> <proof prover="3"><result status="valid" time="0.01" steps="52"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum.7" expl="7. loop invariant preservation" expanded="true"> <goal name="VC maximum.6" expl="6. loop invariant preservation" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter maximum.7.1" expl="1. VC for maximum"> <goal name="VC maximum.6.1" expl="1. VC for maximum">
<proof prover="4"><result status="valid" time="0.01" steps="16"/></proof> <proof prover="3"><result status="valid" time="0.01" steps="19"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum.7.2" expl="2. VC for maximum" expanded="true"> <goal name="VC maximum.6.2" expl="2. VC for maximum">
<proof prover="2"><result status="valid" time="0.78"/></proof> <proof prover="5"><result status="valid" time="2.66"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter maximum.8" expl="8. loop invariant preservation"> <goal name="VC maximum.7" expl="7. loop invariant preservation">
<proof prover="0"><result status="valid" time="4.41"/></proof> <proof prover="1"><result status="valid" time="3.06"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum.9" expl="9. loop invariant preservation"> <goal name="VC maximum.8" expl="8. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.07" steps="74"/></proof> <proof prover="3"><result status="valid" time="0.04" steps="140"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum.10" expl="10. assertion"> <goal name="VC maximum.9" expl="9. assertion">
<proof prover="4"><result status="valid" time="0.01" steps="15"/></proof> <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
</goal> </goal>
<goal name="WP_parameter maximum.11" expl="11. postcondition"> <goal name="VC maximum.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.08"/></proof> <proof prover="3"><result status="valid" time="0.08" steps="153"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter memo" expl="VC for memo"> <goal name="VC memo" expl="VC for memo" expanded="true">
<transf name="split_goal_wp"> <proof prover="3"><result status="valid" time="0.02" steps="90"/></proof>
<goal name="WP_parameter memo.1" expl="1. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter memo.1.1" expl="1. VC for memo">
<proof prover="4"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter memo.1.2" expl="2. VC for memo">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter memo.2" expl="2. variant decrease">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter memo.3" expl="3. precondition">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="WP_parameter memo.4" expl="4. postcondition">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.04" steps="29"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="WP_parameter maxmat" expl="VC for maxmat"> <goal name="VC maxmat" expl="VC for maxmat" expanded="true">
<transf name="split_goal_wp"> <proof prover="3"><result status="valid" time="0.12" steps="222"/></proof>
<goal name="WP_parameter maxmat.1" expl="1. assertion">
<proof prover="4"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter maxmat.2" expl="2. precondition">
<transf name="inline_goal">
<goal name="WP_parameter maxmat.2.1" expl="1. precondition">
<transf name="split_goal_wp">
<goal name="WP_parameter maxmat.2.1.1" expl="1. VC for maxmat">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.2" expl="2. VC for maxmat">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.3" expl="3. VC for maxmat">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.4" expl="4. VC for maxmat">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.5" expl="5. VC for maxmat">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="WP_parameter maxmat.2.1.6" expl="6. VC for maxmat">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter maxmat.3" expl="3. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter maxmat.3.1" expl="1. postcondition">
<transf name="inline_goal">
<goal name="WP_parameter maxmat.3.1.1" expl="1. postcondition">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.10" steps="8"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter maxmat.4" expl="4. postcondition">
<transf name="inline_goal">
<goal name="WP_parameter maxmat.4.1" expl="1. postcondition">
<proof prover="4" timelimit="30" memlimit="0"><result status="valid" time="0.01" steps="36"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal> </goal>
</theory> </theory>
</file> </file>
......
...@@ -2,69 +2,46 @@ ...@@ -2,69 +2,46 @@
<!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="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="3" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../power.mlw" expanded="true"> <file name="../power.mlw" expanded="true">
<theory name="FastExponentiation" sum="4d491a27c69448ee955d4dccb4ef7efb" expanded="true"> <theory name="FastExponentiation" sum="12512f38eb4f6e5ff6ad18e70227844d" expanded="true">
<goal name="WP_parameter fast_exp" expl="VC for fast_exp" expanded="true"> <goal name="VC fast_exp" expl="VC for fast_exp" expanded="true">
<proof prover="4" timelimit="3"><result status="valid" time="0.57" steps="55"/></proof> <proof prover="2"><result status="valid" time="0.18" steps="54"/></proof>
</goal> </goal>
<goal name="WP_parameter fast_exp_imperative" expl="VC for fast_exp_imperative" expanded="true"> <goal name="VC fast_exp_imperative" expl="VC for fast_exp_imperative" expanded="true">
<transf name="split_goal_wp" expanded="true"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter fast_exp_imperative.1" expl="1. loop invariant init" expanded="true"> <goal name="VC fast_exp_imperative.1" expl="1. loop invariant init">
<proof prover="1" timelimit="10"><result status="valid" time="0.00"/></proof> <proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="6"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="WP_parameter fast_exp_imperative.2" expl="2. assertion" expanded="true"> <goal name="VC fast_exp_imperative.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.19" steps="14"/></proof> <proof prover="2"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter fast_exp_imperative.3" expl="3. loop invariant preservation" expanded="true"> <goal name="VC fast_exp_imperative.3" expl="3. precondition">
<transf name="split_goal_wp" expanded="true"> <proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
<goal name="WP_parameter fast_exp_imperative.3.1" expl="1. VC for fast_exp_imperative" expanded="true">
<proof prover="4" timelimit="10" memlimit="1000"><result status="valid" time="0.13" steps="13"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.3.2" expl="2. VC for fast_exp_imperative" expanded="true">
<proof prover="0"><result status="valid" time="2.01" steps="19"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="WP_parameter fast_exp_imperative.4" expl="4. loop variant decrease" expanded="true"> <goal name="VC fast_exp_imperative.4" expl="4. assertion">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.04" steps="12"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="0.22" steps="13"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="WP_parameter fast_exp_imperative.5" expl="5. assertion"> <goal name="VC fast_exp_imperative.5" expl="5. loop variant decrease">
<proof prover="0"><result status="valid" time="0.10" steps="21"/></proof> <proof prover="2"><result status="valid" time="0.49" steps="11"/></proof>
</goal> </goal>
<goal name="WP_parameter fast_exp_imperative.6" expl="6. loop invariant preservation" expanded="true"> <goal name="VC fast_exp_imperative.6" expl="6. loop invariant preservation">
<transf name="split_goal_wp" expanded="true"> <proof prover="2"><result status="valid" time="1.02" steps="32"/></proof>
<goal name="WP_parameter fast_exp_imperative.6.1" expl="1. VC for fast_exp_imperative" expanded="true">
<proof prover="0"><result status="valid" time="0.08" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.6.2" expl="2. VC for fast_exp_imperative" expanded="true">
<proof prover="0"><result status="valid" time="3.10" steps="25"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="WP_parameter fast_exp_imperative.7" expl="7. loop variant decrease" expanded="true"> <goal name="VC fast_exp_imperative.7" expl="7. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="2.38" steps="21"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="WP_parameter fast_exp_imperative.8" expl="8. postcondition" expanded="true"> <goal name="VC fast_exp_imperative.8" expl="8. assertion">
<transf name="split_goal_wp" expanded="true"> <proof prover="2"><result status="valid" time="0.02" steps="18"/></proof>
<goal name="WP_parameter fast_exp_imperative.8.1" expl="1. postcondition" expanded="true"> </goal>
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof> <goal name="VC fast_exp_imperative.9" expl="9. loop variant decrease">
</goal> <proof prover="2"><result status="valid" time="0.26" steps="22"/></proof>
</transf> </goal>
<goal name="VC fast_exp_imperative.10" expl="10. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.24" steps="36"/></proof>
</goal>
<goal name="VC fast_exp_imperative.11" expl="11. postcondition">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -79,7 +79,7 @@ module Shuffle "Knuth shuffle" ...@@ -79,7 +79,7 @@ module Shuffle "Knuth shuffle"
let shuffle (a: array int) : unit let shuffle (a: array int) : unit
writes { a, Random.s } writes { a, Random.s }
ensures { permut_all (old a) a } ensures { permut_all (old a) a }
= for i = 1 to length a - 1 do = "vc:liberal_for" for i = 1 to length a - 1 do
invariant { permut_all (old a) a } invariant { permut_all (old a) a }
swap a i (Random.random_int (i+1)) swap a i (Random.random_int (i+1))
done done
......
This diff is collapsed.
...@@ -2,125 +2,63 @@ ...@@ -2,125 +2,63 @@
<!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="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../selection_sort.mlw"> <file name="../selection_sort.mlw" expanded="true">
<theory name="SelectionSort" sum="b40ac2d5969d58771402c1ba2608bdc1"> <theory name="SelectionSort" sum="2dd84bcc5936acfac763a19996c820d1" expanded="true">
<goal name="WP_parameter selection_sort" expl="VC for selection_sort"> <goal name="VC selection_sort" expl="VC for selection_sort" expanded="true">
<transf name="split_goal_wp"> <transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter selection_sort.1" expl="1. postcondition"> <goal name="VC selection_sort.1" expl="1. loop bounds">
<proof prover="2" timelimit="10" memlimit="0"><result status="valid" time="0.00" steps="9"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.2" expl="2. loop invariant init"> <goal name="VC selection_sort.2" expl="2. loop invariant init">
<proof prover="2" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="11"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.3" expl="3. type invariant"> <goal name="VC selection_sort.3" expl="3. loop bounds">
<proof prover="2"><result status="valid" time="0.01" steps="7"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.4" expl="4. precondition"> <goal name="VC selection_sort.4" expl="4. loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="8"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.5" expl="5. assertion"> <goal name="VC selection_sort.5" expl="5. index in array bounds">
<proof prover="2"><result status="valid" time="0.02" steps="11"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.6" expl="6. loop invariant preservation"> <goal name="VC selection_sort.6" expl="6. index in array bounds">
<transf name="split_goal_wp"> <proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
<goal name="WP_parameter selection_sort.6.1" expl="1. VC for selection_sort">
<proof prover="2"><result status="valid" time="0.08" steps="12"/></proof>
</goal>
<goal name="WP_parameter selection_sort.6.2" expl="2. VC for selection_sort">
<proof prover="2"><result status="valid" time="0.04" steps="12"/></proof>
</goal>
<goal name="WP_parameter selection_sort.6.3" expl="3. VC for selection_sort">
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="WP_parameter selection_sort.7" expl="7. assertion"> <goal name="VC selection_sort.7" expl="7. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="16"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.8" expl="8. loop invariant preservation"> <goal name="VC selection_sort.8" expl="8. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="49"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="23"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.9" expl="9. loop invariant init"> <goal name="VC selection_sort.9" expl="9. precondition">
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.10" expl="10. index in array bounds"> <goal name="VC selection_sort.10" expl="10. assertion">
<proof prover="2"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.11" expl="11. index in array bounds"> <goal name="VC selection_sort.11" expl="11. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="14"/></proof> <proof prover="0"><result status="valid" time="0.58" steps="665"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.12" expl="12. loop invariant preservation"> <goal name="VC selection_sort.12" expl="12. assertion">
<proof prover="2"><result status="valid" time="0.01" steps="36"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="15"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.13" expl="13. loop invariant preservation"> <goal name="VC selection_sort.13" expl="13. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="27"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="93"/></proof>
</goal> </goal>
<goal name="WP_parameter selection_sort.14" expl="14. precondition"> <goal name="VC selection_sort.14" expl="14. postcondition">
<proof prover="2"><result status="valid" time="0.02" steps="11"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="WP_parameter selection_sort.15" expl="15. assertion">
<proof prover="2"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="WP_parameter selection_sort.16" expl="16. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter selection_sort.16.1" expl="1. VC for selection_sort">
<transf name="inline_goal">
<goal name="WP_parameter selection_sort.16.1.1" expl="1. VC for selection_sort">
<transf name="inline_goal">
<goal name="WP_parameter selection_sort.16.1.1.1" expl="1. VC for selection_sort">
<transf name="inline_goal">
<goal name="WP_parameter selection_sort.16.1.1.1.1" expl="1. VC for selection_sort">
<proof prover="2"><result status="valid" time="0.19" steps="302"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter selection_sort.16.2" expl="2. VC for selection_sort">
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter selection_sort.16.3" expl="3. VC for selection_sort">
<transf name="inline_goal">
<goal name="WP_parameter selection_sort.16.3.1" expl="1. VC for selection_sort">
<transf name="inline_goal">
<goal name="WP_parameter selection_sort.16.3.1.1" expl="1. VC for selection_sort">
<transf name="inline_goal">
<goal name="WP_parameter selection_sort.16.3.1.1.1" expl="1. VC for selection_sort">
<proof prover="2"><result status="valid" time="0.35" steps="293"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter selection_sort.17" expl="17. assertion">
<proof prover="2"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter selection_sort.18" expl="18. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.06" steps="55"/></proof>
</goal>
<goal name="WP_parameter selection_sort.19" expl="19. type invariant">
<proof prover="2"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter selection_sort.20" expl="20. postcondition">
<proof prover="2" timelimit="10" memlimit="0"><result status="valid" time="0.02" steps="4"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter test1" expl="VC for test1"> <goal name="VC test1" expl="VC for test1">
<proof prover="2"><result status="valid" time="0.01" steps="6"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter test2" expl="VC for test2"> <goal name="VC test2" expl="VC for test2">
<proof prover="2"><result status="valid" time="0.02" steps="24"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
</goal> </goal>
<goal name="WP_parameter bench" expl="VC for bench"> <goal name="VC bench" expl="VC for bench">
<proof prover="2"><result status="valid" time="0.02" steps="21"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal> </goal>
</theory> </theory>
</file> </file>
......
...@@ -2,20 +2,19 @@ ...@@ -2,20 +2,19 @@
<!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="Alt-Ergo" version="0.99.1" timelimit="6" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../swap.mlw" expanded="true"> <file name="../swap.mlw" expanded="true">
<theory name="Swap" sum="03a7896fac9253beb9bec761b34a8f38" expanded="true"> <theory name="Swap" sum="cfba596a4c6073b18c395dfb76bd786f" expanded="true">
<goal name="WP_parameter swap" expl="VC for swap" expanded="true"> <goal name="VC swap" expl="VC for swap" expanded="true">