Commit 953b3c3e authored by MARCHE Claude's avatar MARCHE Claude

change spec for array update, updates sessions

parent 455499c4
This diff is collapsed.
This diff is collapsed.
......@@ -3,10 +3,10 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../all_distinct.mlw" expanded="true">
<theory name="AllDistinct" sum="29d64b955c0ca1b6353b32886f2fa1d0" expanded="true">
<goal name="VC all_distinct" expl="VC for all_distinct" expanded="true">
<proof prover="0"><result status="valid" time="0.06" steps="273"/></proof>
<file name="../all_distinct.mlw" proved="true">
<theory name="AllDistinct" proved="true" sum="6f38713a3ec25b0a6b1d31017b344871">
<goal name="VC all_distinct" expl="VC for all_distinct" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="270"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,19 +3,19 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../arm.mlw" expanded="true">
<theory name="M" sum="3f4a7332fb862e7e78830642919cdaaf" expanded="true">
<goal name="VC insertion_sort" expl="VC for insertion_sort" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="156"/></proof>
<file name="../arm.mlw" proved="true">
<theory name="M" proved="true" sum="66462041b72873a3bb20b0ae331ca7a0">
<goal name="VC insertion_sort" expl="VC for insertion_sort" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="135"/></proof>
</goal>
</theory>
<theory name="ARM" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="ARM" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="InsertionSortExample" sum="b0bf33c0b21cb5adba7e72e6f7e3acfd" expanded="true">
<goal name="VC path_init_l2" expl="VC for path_init_l2" expanded="true">
<theory name="InsertionSortExample" proved="true" sum="b0bf33c0b21cb5adba7e72e6f7e3acfd">
<goal name="VC path_init_l2" expl="VC for path_init_l2" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="VC path_l2_exit" expl="VC for path_l2_exit" expanded="true">
<goal name="VC path_l2_exit" expl="VC for path_l2_exit" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
</theory>
......
......@@ -9,7 +9,7 @@
</theory>
<theory name="MonoidSum" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="MonoidSumDef" proved="true" sum="fe9dcfe1f224ce795e38a9e5cae32134">
<theory name="MonoidSumDef" proved="true" sum="ad359559eb9e4ed736b1bf8ae16b4f7e">
<goal name="VC agg" expl="VC for agg" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
......
......@@ -7,7 +7,7 @@
<prover id="2" name="Eprover" version="1.8-001" timelimit="20" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../priority_queue.mlw" proved="true">
<theory name="PQueue" proved="true" sum="2dc2e3d764d5c161d843c474061d1d51">
<theory name="PQueue" proved="true" sum="c7511f1fe312a1ffdf3e6f079b7386ed">
<goal name="VC balancing" expl="VC for balancing" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
......@@ -118,10 +118,10 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC monoid_sum_is_min.4.1" expl="VC for monoid_sum_is_min" proved="true">
<proof prover="1"><result status="valid" time="2.38"/></proof>
<proof prover="1"><result status="valid" time="2.77"/></proof>
</goal>
<goal name="VC monoid_sum_is_min.4.2" expl="VC for monoid_sum_is_min" proved="true">
<proof prover="1"><result status="valid" time="1.02"/></proof>
<proof prover="1"><result status="valid" time="1.26"/></proof>
</goal>
</transf>
</goal>
......@@ -138,7 +138,7 @@
<proof prover="0"><result status="valid" time="0.68" steps="1664"/></proof>
</goal>
<goal name="VC selected_is_min.1.1" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="2.30"/></proof>
<proof prover="1"><result status="valid" time="3.76"/></proof>
</goal>
<goal name="VC selected_is_min.1.2" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.47"/></proof>
......@@ -244,7 +244,7 @@
<goal name="VC selected_part.2" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC selected_part.2.0" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="192"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="191"/></proof>
</goal>
<goal name="VC selected_part.2.1" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="73"/></proof>
......@@ -287,7 +287,7 @@
<goal name="VC selected_part.3" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC selected_part.3.0" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="704"/></proof>
<proof prover="0"><result status="valid" time="0.16" steps="703"/></proof>
</goal>
<goal name="VC selected_part.3.1" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="38"/></proof>
......@@ -330,7 +330,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="19"/></proof>
</goal>
<goal name="VC selected_part.3.12" expl="VC for selected_part" proved="true">
<proof prover="0"><result status="valid" time="0.58" steps="1363"/></proof>
<proof prover="0"><result status="valid" time="0.58" steps="1371"/></proof>
</goal>
</transf>
</goal>
......@@ -512,10 +512,10 @@
<proof prover="0"><result status="valid" time="0.03" steps="61"/></proof>
</goal>
<goal name="VC remove_count.1" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="2.02"/></proof>
<proof prover="1"><result status="valid" time="2.41"/></proof>
</goal>
<goal name="VC remove_count.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="6.74"/></proof>
<proof prover="2"><result status="valid" time="7.96"/></proof>
</goal>
</transf>
</goal>
......@@ -584,10 +584,10 @@
<proof prover="0"><result status="valid" time="0.12" steps="76"/></proof>
</goal>
<goal name="VC pop_min.3.1" expl="VC for pop_min" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="1.08" steps="614"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="1.08" steps="613"/></proof>
</goal>
<goal name="VC pop_min.3.2" expl="VC for pop_min" proved="true">
<proof prover="0" timelimit="20"><result status="valid" time="6.54" steps="2313"/></proof>
<proof prover="0" timelimit="20"><result status="valid" time="6.54" steps="2307"/></proof>
</goal>
</transf>
</goal>
......@@ -599,7 +599,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="70"/></proof>
</goal>
<goal name="VC add.1" expl="postcondition" proved="true">
<proof prover="0" timelimit="20"><result status="valid" time="8.04" steps="3503"/></proof>
<proof prover="0" timelimit="20"><result status="valid" time="8.04" steps="3228"/></proof>
</goal>
<goal name="VC add.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
......
......@@ -4,89 +4,97 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" expanded="true">
<theory name="BinarySort" sum="e9d6aae5669e21504778e11633099fa1" expanded="true">
<goal name="VC occ_shift" expl="VC for occ_shift" expanded="true">
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../binary_sort.mlw" proved="true">
<theory name="BinarySort" proved="true" sum="f45759e091adf1bc93196907f82c65a8">
<goal name="VC occ_shift" expl="VC for occ_shift" proved="true">
<proof prover="0"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC binary_sort" expl="VC for binary_sort" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC binary_sort.1" expl="loop invariant init">
<goal name="VC binary_sort" expl="VC for binary_sort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC binary_sort.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="VC binary_sort.2" expl="loop invariant init">
<goal name="VC binary_sort.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC binary_sort.3" expl="index in array bounds">
<goal name="VC binary_sort.2" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC binary_sort.4" expl="loop invariant init">
<goal name="VC binary_sort.3" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC binary_sort.5" expl="loop invariant init">
<goal name="VC binary_sort.4" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC binary_sort.6" expl="loop invariant init">
<goal name="VC binary_sort.5" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC binary_sort.7" expl="precondition">
<goal name="VC binary_sort.6" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC binary_sort.8" expl="index in array bounds">
<goal name="VC binary_sort.7" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="VC binary_sort.9" expl="loop variant decrease">
<goal name="VC binary_sort.8" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="VC binary_sort.10" expl="loop invariant preservation">
<goal name="VC binary_sort.9" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="40"/></proof>
</goal>
<goal name="VC binary_sort.11" expl="loop invariant preservation">
<goal name="VC binary_sort.10" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC binary_sort.12" expl="loop invariant preservation">
<goal name="VC binary_sort.11" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="VC binary_sort.13" expl="loop variant decrease">
<goal name="VC binary_sort.12" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC binary_sort.14" expl="loop invariant preservation">
<goal name="VC binary_sort.13" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC binary_sort.15" expl="loop invariant preservation">
<goal name="VC binary_sort.14" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="22"/></proof>
</goal>
<goal name="VC binary_sort.16" expl="loop invariant preservation">
<goal name="VC binary_sort.15" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="21"/></proof>
</goal>
<goal name="VC binary_sort.17" expl="precondition">
<goal name="VC binary_sort.16" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC binary_sort.18" expl="precondition">
<goal name="VC binary_sort.17" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="VC binary_sort.19" expl="index in array bounds">
<goal name="VC binary_sort.18" expl="index in array bounds" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC binary_sort.20" expl="assertion">
<proof prover="1"><result status="valid" time="0.54" steps="442"/></proof>
<goal name="VC binary_sort.19" expl="assertion" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.50" steps="419"/></proof>
</goal>
<goal name="VC binary_sort.21" expl="assertion">
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
<goal name="VC binary_sort.20" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC binary_sort.22" expl="loop invariant preservation">
<proof prover="1"><result status="valid" time="0.93" steps="845"/></proof>
<goal name="VC binary_sort.21" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(j=k)">
<goal name="VC binary_sort.21.0" expl="loop invariant preservation" proved="true">
<proof prover="1" timelimit="10" memlimit="4000"><result status="valid" time="1.66" steps="1272"/></proof>
</goal>
<goal name="VC binary_sort.21.1" expl="loop invariant preservation" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.75" steps="689"/></proof>
</goal>
</transf>
</goal>
<goal name="VC binary_sort.23" expl="loop invariant preservation">
<proof prover="1"><result status="valid" time="0.03" steps="87"/></proof>
<goal name="VC binary_sort.22" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC binary_sort.24" expl="postcondition">
<goal name="VC binary_sort.23" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC binary_sort.25" expl="postcondition">
<goal name="VC binary_sort.24" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC binary_sort.26" expl="out of loop bounds">
<goal name="VC binary_sort.25" expl="out of loop bounds" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
</goal>
</transf>
......
This diff is collapsed.
This diff is collapsed.
......@@ -5,12 +5,12 @@
<prover id="0" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../braun_trees.mlw" proved="true">
<theory name="BraunHeaps" proved="true" sum="a7a726863662ecf64fe415388da56530">
<theory name="BraunHeaps" proved="true" sum="569e198258de339ee0c9488c19512e7f">
<goal name="VC le_root" expl="VC for le_root" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC root_is_min" expl="VC for root_is_min" proved="true">
<proof prover="1"><result status="valid" time="0.70" steps="1358"/></proof>
<proof prover="1"><result status="valid" time="0.70" steps="1359"/></proof>
</goal>
<goal name="VC empty" expl="VC for empty" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
......@@ -60,7 +60,7 @@
<proof prover="1"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC replace_min.11" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="3.78" steps="10225"/></proof>
<proof prover="1"><result status="valid" time="3.78" steps="10045"/></proof>
</goal>
<goal name="VC replace_min.12" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.08" steps="556"/></proof>
......
......@@ -3,94 +3,94 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bubble_sort.mlw" expanded="true">
<theory name="BubbleSort" sum="2b49bf699bc92f5af1fe643dca62b3f9" 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="loop invariant init">
<file name="../bubble_sort.mlw" proved="true">
<theory name="BubbleSort" proved="true" sum="3652d10a9dbb20e7dbddea3c6210177c">
<goal name="VC bubble_sort" expl="VC for bubble_sort" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC bubble_sort.0" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC bubble_sort.2" expl="loop invariant init">
<goal name="VC bubble_sort.1" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC bubble_sort.3" expl="loop invariant init">
<goal name="VC bubble_sort.2" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC bubble_sort.4" expl="loop invariant init">
<goal name="VC bubble_sort.3" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC bubble_sort.5" expl="loop invariant init">
<goal name="VC bubble_sort.4" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC bubble_sort.6" expl="loop invariant init">
<goal name="VC bubble_sort.5" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
</goal>
<goal name="VC bubble_sort.7" expl="loop invariant init">
<goal name="VC bubble_sort.6" expl="loop invariant init" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC bubble_sort.8" expl="index in array bounds">
<goal name="VC bubble_sort.7" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC bubble_sort.9" expl="index in array bounds">
<goal name="VC bubble_sort.8" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC bubble_sort.10" expl="precondition">
<goal name="VC bubble_sort.9" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="VC bubble_sort.11" expl="loop invariant preservation">
<goal name="VC bubble_sort.10" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="151"/></proof>
</goal>
<goal name="VC bubble_sort.12" expl="loop invariant preservation">
<goal name="VC bubble_sort.11" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="179"/></proof>
</goal>
<goal name="VC bubble_sort.13" expl="loop invariant preservation">
<goal name="VC bubble_sort.12" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.18" steps="383"/></proof>
</goal>
<goal name="VC bubble_sort.14" expl="loop invariant preservation">
<goal name="VC bubble_sort.13" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="103"/></proof>
</goal>
<goal name="VC bubble_sort.15" expl="loop invariant preservation">
<goal name="VC bubble_sort.14" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC bubble_sort.16" expl="loop invariant preservation">
<goal name="VC bubble_sort.15" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC bubble_sort.17" expl="loop invariant preservation">
<goal name="VC bubble_sort.16" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC bubble_sort.18" expl="loop invariant preservation">
<goal name="VC bubble_sort.17" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="VC bubble_sort.19" expl="loop invariant preservation">
<goal name="VC bubble_sort.18" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC bubble_sort.20" expl="loop invariant preservation">
<goal name="VC bubble_sort.19" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="42"/></proof>
</goal>
<goal name="VC bubble_sort.21" expl="loop invariant preservation">
<goal name="VC bubble_sort.20" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="VC bubble_sort.22" expl="out of loop bounds">
<goal name="VC bubble_sort.21" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC bubble_sort.23" expl="postcondition">
<goal name="VC bubble_sort.22" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC bubble_sort.24" expl="postcondition">
<goal name="VC bubble_sort.23" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC bubble_sort.25" expl="out of loop bounds">
<goal name="VC bubble_sort.24" expl="out of loop bounds" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="VC test1" expl="VC for test1" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
<goal name="VC test1" expl="VC for test1" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="VC test2" expl="VC for test2" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
<goal name="VC test2" expl="VC for test2" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="38"/></proof>
</goal>
<goal name="VC bench" expl="VC for bench" expanded="true">
<goal name="VC bench" expl="VC for bench" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
</theory>
......
......@@ -3,17 +3,17 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../conjugate.mlw" expanded="true">
<theory name="Conjugate" sum="18382f4f171724c051985bfdff9a47b7" expanded="true">
<goal name="VC conjugate" expl="VC for conjugate" expanded="true">
<proof prover="0"><result status="valid" time="0.13" steps="316"/></proof>
<file name="../conjugate.mlw" proved="true">
<theory name="Conjugate" proved="true" sum="a4627d5b4c10a678bd8f3ac4153e1701">
<goal name="VC conjugate" expl="VC for conjugate" proved="true">
<proof prover="0"><result status="valid" time="0.13" steps="318"/></proof>
</goal>
</theory>
<theory name="Test" sum="143b95196fccc06b9d4eab84a6f33f73" expanded="true">
<goal name="VC test" expl="VC for test" expanded="true">
<proof prover="0"><result status="valid" time="0.11" steps="181"/></proof>
<theory name="Test" proved="true" sum="7ce01eb912fe3360b61ea4643591d3f0">
<goal name="VC test" expl="VC for test" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="96"/></proof>
</goal>
<goal name="VC bench" expl="VC for bench" expanded="true">
<goal name="VC bench" expl="VC for bench" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
</theory>
......
This diff is collapsed.
This diff is collapsed.
......@@ -3,21 +3,21 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../fenwick.mlw" expanded="true">
<theory name="Fenwick" sum="760b357064818191988c3d175c5d6a2f" expanded="true">
<goal name="VC make" expl="VC for make">
<file name="../fenwick.mlw" proved="true">
<theory name="Fenwick" proved="true" sum="25a9b8a570abe4fad2d18660a29171c4">
<goal name="VC make" expl="VC for make" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC add" expl="VC for add">
<proof prover="1"><result status="valid" time="0.66" steps="807"/></proof>
<goal name="VC add" expl="VC for add" proved="true">
<proof prover="1"><result status="valid" time="0.66" steps="721"/></proof>
</goal>
<goal name="VC sum_dec" expl="VC for sum_dec">
<goal name="VC sum_dec" expl="VC for sum_dec" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="37"/></proof>
</goal>
<goal name="VC fen_compact" expl="VC for fen_compact">
<goal name="VC fen_compact" expl="VC for fen_compact" proved="true">
<proof prover="1"><result status="valid" time="0.82" steps="850"/></proof>
</goal>
<goal name="VC query" expl="VC for query">
<goal name="VC query" expl="VC for query" proved="true">
<proof prover="1"><result status="valid" time="2.57" steps="2527"/></proof>
</goal>
</theory>
......
......@@ -3,10 +3,10 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<file name="../fill.mlw" expanded="true">
<theory name="Fill" sum="0508df762fb55f16bdf36b85f0d008a6" expanded="true">
<goal name="VC fill" expl="VC for fill" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="150"/></proof>
<file name="../fill.mlw" proved="true">
<theory name="Fill" proved="true" sum="dad196c903de8fcac5ba6fb18a5d7269">
<goal name="VC fill" expl="VC for fill" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="146"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,126 +3,126 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../find.mlw" expanded="true">
<theory name="FIND" sum="a0ad71b8b7443ce2478b29de2d155667" expanded="true">
<goal name="VC _N" expl="VC for _N">
<file name="../find.mlw" proved="true">
<theory name="FIND" proved="true" sum="75e4da35bcfff9f53aa3139c022463b5">
<goal name="VC _N" expl="VC for _N" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC f" expl="VC for f">
<goal name="VC f" expl="VC for f" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC find" expl="VC for find" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC find.1" expl="loop invariant init">
<goal name="VC find" expl="VC for find" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC find.0" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC find.2" expl="index in array bounds">
<goal name="VC find.1" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC find.3" expl="loop invariant init">
<goal name="VC find.2" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="65"/></proof>
</goal>
<goal name="VC find.4" expl="loop invariant init">
<goal name="VC find.3" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC find.5" expl="index in array bounds">
<goal name="VC find.4" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="33"/></proof>
</goal>
<goal name="VC find.6" expl="loop variant decrease">
<goal name="VC find.5" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="VC find.7" expl="loop invariant preservation">
<goal name="VC find.6" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.08" steps="86"/></proof>
</goal>
<goal name="VC find.8" expl="loop invariant init">
<goal name="VC find.7" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="VC find.9" expl="index in array bounds">
<goal name="VC find.8" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="31"/></proof>
</goal>
<goal name="VC find.10" expl="loop variant decrease">
<goal name="VC find.9" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="VC find.11" expl="loop invariant preservation">
<goal name="VC find.10" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="96"/></proof>
</goal>
<goal name="VC find.12" expl="assertion">
<goal name="VC find.11" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="31"/></proof>
</goal>
<goal name="VC find.13" expl="index in array bounds">
<goal name="VC find.12" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="43"/></proof>
</goal>
<goal name="VC find.14" expl="index in array bounds">
<goal name="VC find.13" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="VC find.15" expl="index in array bounds">
<goal name="VC find.14" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="43"/></proof>
</goal>
<goal name="VC find.16" expl="index in array bounds">
<proof prover="2"><result status="valid" time="0.01" steps="37"/></proof>
<goal name="VC find.15" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="38"/></proof>
</goal>
<goal name="VC find.17" expl="assertion">