Commit 1e331507 authored by Martin Clochard's avatar Martin Clochard

examples: update provers for avl example

parent cf4020c5
......@@ -2,70 +2,69 @@
<!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="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../association_list.mlw" expanded="true">
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../association_list.mlw">
<theory name="Assoc" sum="12adb5d5e7c156493bafb1bd121c4586">
<goal name="appear_append">
<proof prover="4"><result status="valid" time="0.03" steps="67"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="48"/></proof>
</goal>
<goal name="WP_parameter model_domain" expl="VC for model_domain">
<proof prover="4"><result status="valid" time="0.07" steps="233"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="274"/></proof>
</goal>
<goal name="WP_parameter model_key" expl="VC for model_key">
<proof prover="4"><result status="valid" time="0.04" steps="124"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="103"/></proof>
</goal>
<goal name="WP_parameter model_congruence" expl="VC for model_congruence">
<transf name="split_goal_wp">
<goal name="WP_parameter model_congruence.1" expl="1. variant decrease">
<proof prover="4"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter model_congruence.2" expl="2. precondition">
<proof prover="4"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="WP_parameter model_congruence.3" expl="3. postcondition">
<proof prover="4"><result status="valid" time="0.08" steps="194"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="127"/></proof>
</goal>
<goal name="WP_parameter model_congruence.4" expl="4. postcondition">
<proof prover="4"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter model_unique" expl="VC for model_unique">
<proof prover="4"><result status="valid" time="0.03" steps="160"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="108"/></proof>
</goal>
<goal name="WP_parameter model_singleton" expl="VC for model_singleton">
<proof prover="4"><result status="valid" time="0.02" steps="41"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="70"/></proof>
</goal>
<goal name="WP_parameter model_concat" expl="VC for model_concat">
<transf name="split_goal_wp">
<goal name="WP_parameter model_concat.1" expl="1. postcondition">
<proof prover="4"><result status="valid" time="0.03" steps="70"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="24"/></proof>
</goal>
<goal name="WP_parameter model_concat.2" expl="2. postcondition">
<proof prover="4"><result status="valid" time="0.03" steps="75"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="22"/></proof>
</goal>
<goal name="WP_parameter model_concat.3" expl="3. postcondition">
<proof prover="4"><result status="valid" time="0.03" steps="39"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="23"/></proof>
</goal>
<goal name="WP_parameter model_concat.4" expl="4. postcondition">
<proof prover="4"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter model_concat.5" expl="5. variant decrease">
<proof prover="4"><result status="valid" time="0.02" steps="29"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter model_concat.6" expl="6. precondition">
<proof prover="4"><result status="valid" time="0.02" steps="55"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="WP_parameter model_concat.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.45"/></proof>
<proof prover="1"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="WP_parameter model_concat.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter model_concat.9" expl="9. postcondition">
<proof prover="4"><result status="valid" time="0.09" steps="115"/></proof>
<proof prover="4"><result status="valid" time="0.09" steps="143"/></proof>
</goal>
<goal name="WP_parameter model_concat.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
......@@ -73,26 +72,26 @@
</transf>
</goal>
</theory>
<theory name="AssocSorted" sum="c234d7458c225ff847c0ef368a2e5830" expanded="true">
<goal name="Eq.Refl" expanded="true">
<theory name="AssocSorted" sum="c234d7458c225ff847c0ef368a2e5830">
<goal name="Eq.Refl">
<proof prover="4"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="Eq.Trans" expanded="true">
<goal name="Eq.Trans">
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="Eq.Symm" expanded="true">
<goal name="Eq.Symm">
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="S.O.Trans" expanded="true">
<goal name="S.O.Trans">
<proof prover="4"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter increasing_unique" expl="VC for increasing_unique">
<proof prover="4"><result status="valid" time="0.07" steps="85"/></proof>
<proof prover="4"><result status="valid" time="0.07" steps="66"/></proof>
</goal>
<goal name="WP_parameter model_cut" expl="VC for model_cut">
<transf name="split_goal_wp">
<goal name="WP_parameter model_cut.1" expl="1. assertion">
<proof prover="4"><result status="valid" time="0.04" steps="63"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="66"/></proof>
</goal>
<goal name="WP_parameter model_cut.2" expl="2. assertion">
<transf name="split_goal_wp">
......@@ -100,16 +99,16 @@
<proof prover="4"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.2" expl="2. assertion">
<proof prover="4"><result status="valid" time="0.08" steps="125"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="106"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.3" expl="3. assertion">
<proof prover="4"><result status="valid" time="0.02" steps="123"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="106"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.4" expl="4. assertion">
<proof prover="4"><result status="valid" time="0.02" steps="0"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.5" expl="5. assertion">
<proof prover="4"><result status="valid" time="0.03" steps="41"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="32"/></proof>
</goal>
<goal name="WP_parameter model_cut.2.6" expl="6. assertion">
<proof prover="4"><result status="valid" time="0.08" steps="0"/></proof>
......@@ -122,10 +121,10 @@
<proof prover="4"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.2" expl="2. assertion">
<proof prover="4"><result status="valid" time="0.08" steps="122"/></proof>
<proof prover="4"><result status="valid" time="0.08" steps="104"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.3" expl="3. assertion">
<proof prover="4"><result status="valid" time="0.02" steps="152"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="136"/></proof>
</goal>
<goal name="WP_parameter model_cut.3.4" expl="4. assertion">
<proof prover="4"><result status="valid" time="0.02" steps="0"/></proof>
......@@ -158,18 +157,18 @@
<proof prover="4"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="WP_parameter model_cut.7" expl="7. postcondition">
<proof prover="4"><result status="valid" time="0.13" steps="136"/></proof>
<proof prover="4"><result status="valid" time="0.13" steps="145"/></proof>
</goal>
<goal name="WP_parameter model_cut.8" expl="8. postcondition">
<proof prover="4"><result status="valid" time="0.03" steps="8"/></proof>
</goal>
<goal name="WP_parameter model_cut.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="4" steplimit="0"><result status="valid" time="0.11" steps="312"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter model_split" expl="VC for model_split">
<proof prover="0"><result status="valid" time="1.89"/></proof>
<proof prover="4" steplimit="0"><result status="valid" time="0.15" steps="686"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../monoid.mlw">
<theory name="Monoid" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
......
......@@ -2,34 +2,34 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="1" memlimit="1000"/>
<file name="../preorder.mlw" expanded="true">
<theory name="Full" sum="41eddb6a5f9e7172479be99f6dc563ca" expanded="true">
<goal name="Eq.Refl" expanded="true">
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="3" steplimit="1" memlimit="1000"/>
<file name="../preorder.mlw">
<theory name="Full" sum="41eddb6a5f9e7172479be99f6dc563ca">
<goal name="Eq.Refl">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="Eq.Trans" expanded="true">
<goal name="Eq.Trans">
<proof prover="1"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="Eq.Symm" expanded="true">
<goal name="Eq.Symm">
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="Lt.Trans" expanded="true">
<goal name="Lt.Trans">
<proof prover="1"><result status="valid" time="0.03" steps="35"/></proof>
</goal>
<goal name="Lt.Asymm" expanded="true">
<goal name="Lt.Asymm">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</theory>
<theory name="TotalFull" sum="b7a34af67ae9cf9bf55e6d6a58a0f423" expanded="true">
<goal name="Lt.Total" expanded="true">
<theory name="TotalFull" sum="b7a34af67ae9cf9bf55e6d6a58a0f423">
<goal name="Lt.Total">
<proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="lt_def2" expanded="true">
<goal name="lt_def2">
<proof prover="1" timelimit="5"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
</theory>
<theory name="Computable" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Computable" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
</file>
</why3session>
......@@ -143,7 +143,10 @@ module PQueue
| Some k -> CO.eq d.key k
end
end }
= ()
= match e.middle with
| None -> absurd
| Some d -> assert { S.lower_bound d.key e.right && CO.le d.key d.key }
end
let selected_part (ghost llis:list (D.t 'a))
(ghost rlis:list (D.t 'a))
......
This diff is collapsed.
......@@ -2,10 +2,9 @@
<!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="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../ral.mlw" expanded="true">
<theory name="RAL" sum="c7ad4c6b81728dbd18a1c23ee5747ec2" expanded="true">
<prover id="2" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../ral.mlw">
<theory name="RAL" sum="c7ad4c6b81728dbd18a1c23ee5747ec2">
<goal name="M.assoc">
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
......@@ -28,10 +27,10 @@
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
<goal name="WP_parameter sum_measure_is_length" expl="VC for sum_measure_is_length">
<proof prover="2"><result status="valid" time="0.02" steps="33"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter selected_part" expl="VC for selected_part">
<proof prover="2"><result status="valid" time="0.04" steps="96"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="87"/></proof>
</goal>
<goal name="Sel.M.assoc">
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="1"/></proof>
......@@ -40,16 +39,16 @@
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
<goal name="Sel.M.sum_def_nil">
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="4"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="Sel.M.sum_def_cons">
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="6"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="2"/></proof>
</goal>
<goal name="Sel.balancing_positive">
<proof prover="2" timelimit="3"><result status="valid" time="0.02" steps="1"/></proof>
</goal>
<goal name="Sel.selection_empty">
<proof prover="2" timelimit="3"><result status="valid" time="0.04" steps="27"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.04" steps="16"/></proof>
</goal>
<goal name="Sel.WP_parameter avl AVL M zero" expl="VC for avl AVL M zero">
<proof prover="2" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
......@@ -58,10 +57,10 @@
<proof prover="2" timelimit="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="Sel.WP_parameter avl AVL D measure" expl="VC for avl AVL D measure">
<proof prover="2" timelimit="3"><result status="valid" time="0.03" steps="3"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.03" steps="2"/></proof>
</goal>
<goal name="Sel.WP_parameter avl AVL selected_part" expl="VC for avl AVL selected_part">
<proof prover="2" timelimit="3"><result status="valid" time="0.34" steps="534"/></proof>
<proof prover="2" timelimit="3"><result status="valid" time="0.05" steps="204"/></proof>
</goal>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="2"><result status="valid" time="0.02" steps="4"/></proof>
......@@ -70,13 +69,13 @@
<proof prover="2"><result status="valid" time="0.03" steps="4"/></proof>
</goal>
<goal name="WP_parameter is_empty" expl="VC for is_empty">
<proof prover="2"><result status="valid" time="0.03" steps="23"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="11"/></proof>
</goal>
<goal name="WP_parameter decompose_front" expl="VC for decompose_front">
<proof prover="2"><result status="valid" time="0.04" steps="66"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="WP_parameter decompose_back" expl="VC for decompose_back">
<proof prover="2"><result status="valid" time="0.04" steps="74"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="47"/></proof>
</goal>
<goal name="WP_parameter front" expl="VC for front">
<proof prover="2"><result status="valid" time="0.02" steps="3"/></proof>
......@@ -94,18 +93,18 @@
<proof prover="2"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
<goal name="WP_parameter length" expl="VC for length">
<proof prover="2"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter set" expl="VC for set">
<transf name="split_goal_wp">
<goal name="WP_parameter set.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="9"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter set.2" expl="2. postcondition">
<proof prover="2"><result status="valid" time="0.12" steps="87"/></proof>
<proof prover="2"><result status="valid" time="0.12" steps="80"/></proof>
</goal>
<goal name="WP_parameter set.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="1.25" steps="284"/></proof>
<proof prover="2"><result status="valid" time="0.34" steps="534"/></proof>
</goal>
<goal name="WP_parameter set.4" expl="4. postcondition">
<proof prover="2"><result status="valid" time="0.04" steps="43"/></proof>
......@@ -113,19 +112,19 @@
</transf>
</goal>
<goal name="WP_parameter get" expl="VC for get">
<proof prover="2"><result status="valid" time="0.14" steps="78"/></proof>
<proof prover="2"><result status="valid" time="0.14" steps="116"/></proof>
</goal>
<goal name="WP_parameter insert" expl="VC for insert">
<proof prover="2"><result status="valid" time="0.58" steps="304"/></proof>
<proof prover="2"><result status="valid" time="0.13" steps="329"/></proof>
</goal>
<goal name="WP_parameter remove" expl="VC for remove">
<proof prover="0"><result status="valid" time="0.45"/></proof>
<proof prover="2" steplimit="0"><result status="valid" time="0.15" steps="346"/></proof>
</goal>
<goal name="WP_parameter cut" expl="VC for cut">
<proof prover="2"><result status="valid" time="0.05" steps="52"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="46"/></proof>
</goal>
<goal name="WP_parameter split" expl="VC for split">
<proof prover="2"><result status="valid" time="0.05" steps="66"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="59"/></proof>
</goal>
<goal name="WP_parameter harness" expl="VC for harness">
<transf name="split_goal_wp">
......@@ -142,10 +141,10 @@
<proof prover="2"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter harness.5" expl="5. check">
<proof prover="2"><result status="valid" time="0.07" steps="98"/></proof>
<proof prover="2"><result status="valid" time="0.07" steps="133"/></proof>
</goal>
<goal name="WP_parameter harness.6" expl="6. check">
<proof prover="2"><result status="valid" time="0.07" steps="96"/></proof>
<proof prover="2"><result status="valid" time="0.07" steps="131"/></proof>
</goal>
<goal name="WP_parameter harness.7" expl="7. precondition">
<proof prover="2"><result status="valid" time="0.04" steps="23"/></proof>
......@@ -154,10 +153,10 @@
<proof prover="2"><result status="valid" time="0.03" steps="26"/></proof>
</goal>
<goal name="WP_parameter harness.9" expl="9. check">
<proof prover="2"><result status="valid" time="0.17" steps="127"/></proof>
<proof prover="2"><result status="valid" time="0.17" steps="169"/></proof>
</goal>
<goal name="WP_parameter harness.10" expl="10. check">
<proof prover="2"><result status="valid" time="0.26" steps="203"/></proof>
<proof prover="2"><result status="valid" time="0.06" steps="199"/></proof>
</goal>
</transf>
</goal>
......@@ -173,16 +172,16 @@
<proof prover="2"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter harness2.4" expl="4. unreachable point">
<proof prover="2"><result status="valid" time="0.04" steps="48"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="27"/></proof>
</goal>
<goal name="WP_parameter harness2.5" expl="5. check">
<proof prover="2"><result status="valid" time="0.05" steps="98"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="59"/></proof>
</goal>
<goal name="WP_parameter harness2.6" expl="6. precondition">
<proof prover="2"><result status="valid" time="0.05" steps="135"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="30"/></proof>
</goal>
<goal name="WP_parameter harness2.7" expl="7. check">
<proof prover="2"><result status="valid" time="0.16" steps="159"/></proof>
<proof prover="2"><result status="valid" time="0.16" steps="108"/></proof>
</goal>
</transf>
</goal>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../sorted.mlw">
<theory name="Increasing" sum="33bff6ba91e99a4e930bd71eb88f6a0e">
<goal name="smaller_lower_bound">
......
This diff is collapsed.
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