Commit 4f8926c2 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Session files for dijkstra and sumrange updated

parent 846ee30c
......@@ -3,20 +3,19 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../dijkstra.mlw" proved="true">
<theory name="DijkstraShortestPath" proved="true" sum="501f8eee126b36613e1204b6238c589f">
<goal name="WP_parameter relax" expl="VC for relax" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="Length_nonneg" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="Length_nonneg.0" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="Length_nonneg.1" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -24,37 +23,36 @@
</transf>
</goal>
<goal name="Path_inversion" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="Path_shortest_path" proved="true">
<transf name="assert" proved="true" arg1="(forall sn. forall d. 0 &lt;= d &lt; sn -&gt; forall v. path src v d -&gt; exists d&apos;:int. shortest_path src v d&apos; /\ d&apos; &lt;= d)">
<goal name="Path_shortest_path.0" proved="true">
<transf name="induction" proved="true" arg1="sn">
<goal name="Path_shortest_path.0.0" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Path_shortest_path.0.1" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="sn">
<goal name="Path_shortest_path.0.1.0" proved="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.04"/></proof>
<proof prover="4" timelimit="5"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="Path_shortest_path.1" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="Main_lemma" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="173"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="173"/></proof>
</goal>
<goal name="Completeness_lemma" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="Completeness_lemma.0" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Completeness_lemma.1" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......@@ -64,15 +62,15 @@
<goal name="inside_or_exit" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="inside_or_exit.0" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="inside_or_exit.1" proved="true">
<transf name="case" proved="true" arg1="(mem z s)">
<goal name="inside_or_exit.1.0" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inside_or_exit.1.1" proved="true">
<proof prover="5"><result status="valid" time="0.84"/></proof>
<proof prover="4"><result status="valid" time="0.84"/></proof>
</goal>
</transf>
</goal>
......@@ -81,73 +79,73 @@
<goal name="WP_parameter shortest_path_code" expl="VC for shortest_path_code" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter shortest_path_code.0" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="164"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="164"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.1" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.2" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.3" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.4" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="86"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.5" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.6" expl="loop invariant init" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.08" steps="321"/></proof>
<proof prover="1" timelimit="1"><result status="valid" time="0.08" steps="321"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.7" expl="loop invariant init" proved="true">
<proof prover="2" timelimit="60"><result status="valid" time="0.02" steps="110"/></proof>
<proof prover="1" timelimit="60"><result status="valid" time="0.02" steps="110"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.8" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.9" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.18"/></proof>
<proof prover="2"><result status="valid" time="0.18"/></proof>
<transf name="remove" proved="true" arg1="real,tuple0,unit,ref,zero,one,(&gt;),(-),( * ),(-),(==),singleton,union,inter,diff,choose,(!),Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Select_eq,Select_neq,extensionality,subset_refl,subset_trans,empty_def1,mem_empty,remove_def1,add_remove,remove_add,subset_remove,union_def1,inter_def1,diff_def1,subset_diff,choose_def,cardinal_nonneg,cardinal_empty,cardinal_add,cardinal_remove,subset_eq,cardinal1,G_succ_sound,Weight_nonneg,Length_nonneg,Path_inversion,Path_shortest_path,Main_lemma,Completeness_lemma,inside_or_exit">
<goal name="WP_parameter shortest_path_code.9.0" expl="assertion" proved="true">
<proof prover="3" timelimit="1"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.10" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="40"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="40"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11" expl="loop invariant preservation" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="WP_parameter shortest_path_code.11.0" expl="loop invariant preservation" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter shortest_path_code.11.0.0" expl="VC for shortest_path_code" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="64"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="64"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.1" expl="VC for shortest_path_code" proved="true">
<proof prover="0" timelimit="10" memlimit="4000"><result status="valid" time="1.40"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.2" expl="VC for shortest_path_code" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.3" expl="VC for shortest_path_code" proved="true">
<proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="8.42"/></proof>
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="8.42"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.4" expl="VC for shortest_path_code" proved="true">
<proof prover="2"><result status="valid" time="0.05" steps="191"/></proof>
<proof prover="1"><result status="valid" time="0.05" steps="191"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.5" expl="VC for shortest_path_code" proved="true">
<proof prover="2"><result status="valid" time="0.17" steps="495"/></proof>
<proof prover="1"><result status="valid" time="0.17" steps="495"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6" expl="VC for shortest_path_code" proved="true">
<transf name="case" proved="true" arg1="(v = v1)">
<goal name="WP_parameter shortest_path_code.11.0.6.0" expl="VC for shortest_path_code" proved="true">
<proof prover="4"><result status="valid" time="0.70"/></proof>
<proof prover="3"><result status="valid" time="0.70"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.1" expl="VC for shortest_path_code" proved="true">
<proof prover="5"><result status="valid" time="0.12"/></proof>
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
</goal>
......@@ -156,16 +154,16 @@
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.12" expl="loop invariant preservation" proved="true">
<proof prover="5"><result status="valid" time="0.20"/></proof>
<proof prover="4"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.13" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="59"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="59"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.14" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.15" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.10" steps="291"/></proof>
<proof prover="1"><result status="valid" time="0.10" steps="291"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.16" expl="loop invariant preservation" proved="true">
<transf name="introduce_premises" proved="true" >
......@@ -174,28 +172,28 @@
<goal name="WP_parameter shortest_path_code.16.0.0" expl="loop invariant preservation" proved="true">
<transf name="cut" proved="true" arg1="(inv_succ src visited q d)">
<goal name="WP_parameter shortest_path_code.16.0.0.0" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.39"/></proof>
<proof prover="3"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.0.1" proved="true">
<proof prover="5"><result status="valid" time="0.08"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.1" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.17" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="122"/></proof>
<proof prover="1"><result status="valid" time="0.04" steps="122"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.18" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.19" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.18" steps="352"/></proof>
<proof prover="1"><result status="valid" time="0.18" steps="352"/></proof>
</goal>
</transf>
</goal>
......
......@@ -7,7 +7,7 @@
<prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../sumrange.mlw" proved="true">
<theory name="ArraySum" proved="true" sum="c43abcc65051af09a54f471f27f69208">
<theory name="ArraySum" proved="true" sum="9c589f5858612dacf098c9434ffb74c2">
<goal name="sum_right" proved="true">
<transf name="assert" proved="true" arg1="(forall x. 0 &lt; x &lt; j -&gt; sum a (j-x) j = sum a (j-x) (j-1) + a[j-1])">
<goal name="sum_right.0" proved="true">
......@@ -16,7 +16,11 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sum_right.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="instantiate" proved="true" arg1="Hrec" arg2="x">
<goal name="sum_right.0.1.0" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
......@@ -30,7 +34,7 @@
</transf>
</goal>
</theory>
<theory name="Simple" proved="true" sum="17809040d6493313e8bff554cd196ef3">
<theory name="Simple" proved="true" sum="4c20541d262bc9deec1ea3531579a715">
<goal name="WP_parameter query" expl="VC for query" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
......@@ -59,14 +63,18 @@
</transf>
</goal>
</theory>
<theory name="ExtraLemmas" proved="true" sum="06d9ed7291283643f4ece6e481eb7dd6">
<theory name="ExtraLemmas" proved="true" sum="19e80bf42f3115702df43c625a5b4d12">
<goal name="sum_concat" proved="true">
<transf name="induction" proved="true" arg1="k">
<goal name="sum_concat.0" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sum_concat.1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="instantiate" proved="true" arg1="Hrec" arg2="k">
<goal name="sum_concat.1.0" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
......@@ -78,7 +86,11 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sum_frame.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<transf name="instantiate" proved="true" arg1="Hrec" arg2="x">
<goal name="sum_frame.0.1.0" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
......@@ -103,7 +115,7 @@
<goal name="sum_update.1" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="sum_update.1.0" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
......@@ -121,7 +133,7 @@
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
<theory name="CumulativeTree" proved="true" sum="27ac94e51ac30faab1b36fe9f2a7393a">
<theory name="CumulativeTree" proved="true" sum="27793b09427965c733ab65af79f4722e">
<goal name="WP_parameter tree_of_array" expl="VC for tree_of_array" proved="true">
<proof prover="3"><result status="valid" time="0.43"/></proof>
</goal>
......
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