Commit ce3f04f6 authored by MARCHE Claude's avatar MARCHE Claude

fix sessions impacted by absence of implicit introduction of premises

parent fd475360
......@@ -26,12 +26,16 @@
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="Path_shortest_path" proved="true">
<transf name="induction" proved="true" arg1="d">
<goal name="Path_shortest_path.0" expl="base case" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Path_shortest_path.1" expl="recursive case" proved="true">
<proof prover="4" timelimit="5"><result status="valid" time="0.06"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="Path_shortest_path.0" proved="true">
<transf name="induction" proved="true" arg1="d">
<goal name="Path_shortest_path.0.0" expl="base case" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="Path_shortest_path.0.1" expl="recursive case" proved="true">
<proof prover="4" timelimit="5"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
......@@ -54,12 +58,16 @@
<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" expl="true case" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inside_or_exit.1.1" expl="false case" proved="true">
<proof prover="4"><result status="valid" time="0.84"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="inside_or_exit.1.0" proved="true">
<transf name="case" proved="true" arg1="(mem z s)">
<goal name="inside_or_exit.1.0.0" expl="true case" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="inside_or_exit.1.0.1" expl="false case" proved="true">
<proof prover="4"><result status="valid" time="0.91"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
......@@ -129,12 +137,16 @@
<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="true case" proved="true">
<proof prover="3"><result status="valid" time="0.70"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.1" expl="false case" proved="true">
<proof prover="4"><result status="valid" time="0.12"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="WP_parameter shortest_path_code.11.0.6.0" 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.0" expl="true case" proved="true">
<proof prover="3"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.0.1" expl="false case" proved="true">
<proof prover="4"><result status="valid" time="0.21"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
......@@ -155,20 +167,24 @@
<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="cut" proved="true" arg1="(is_empty su)">
<transf name="introduce_premises" proved="true" >
<goal name="WP_parameter shortest_path_code.16.0" expl="loop invariant preservation" proved="true">
<transf name="cut" proved="true" arg1="(inv_succ src visited q d)">
<transf name="cut" proved="true" arg1="(is_empty su)">
<goal name="WP_parameter shortest_path_code.16.0.0" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.35"/></proof>
<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="3"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.0.1" proved="true">
<proof prover="4"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.1" proved="true">
<proof prover="4"><result status="valid" time="0.13"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.16.1" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.17" expl="loop variant decrease" proved="true">
......
......@@ -13,30 +13,34 @@
<file name="../euler001.mlw" proved="true">
<theory name="DivModHints" proved="true">
<goal name="mod_div_unique" proved="true">
<transf name="assert" proved="true" arg1="(q - div x y) * y + (r - mod x y) = 0">
<transf name="introduce_premises" proved="true" >
<goal name="mod_div_unique.0" proved="true">
<proof prover="5" timelimit="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="mod_div_unique.1" proved="true">
<transf name="case" proved="true" arg1="q - div x y &gt;= 1">
<goal name="mod_div_unique.1.0" expl="true case" proved="true">
<proof prover="6"><result status="valid" time="0.11"/></proof>
<transf name="assert" proved="true" arg1="(q - div x y) * y + (r - mod x y) = 0">
<goal name="mod_div_unique.0.0" proved="true">
<proof prover="5" timelimit="1" memlimit="1000"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="mod_div_unique.1.1" expl="false case" proved="true">
<transf name="case" proved="true" arg1="q - div x y &lt;= -1">
<goal name="mod_div_unique.1.1.0" expl="false case (true case)" proved="true">
<transf name="assert" proved="true" arg1="(y * (q - div x y) &lt;= - y)">
<goal name="mod_div_unique.1.1.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.46"/></proof>
<goal name="mod_div_unique.0.1" proved="true">
<transf name="case" proved="true" arg1="q - div x y &gt;= 1">
<goal name="mod_div_unique.0.1.0" expl="true case" proved="true">
<proof prover="6"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="mod_div_unique.0.1.1" expl="false case" proved="true">
<transf name="case" proved="true" arg1="q - div x y &lt;= -1">
<goal name="mod_div_unique.0.1.1.0" expl="false case (true case)" proved="true">
<transf name="assert" proved="true" arg1="(y * (q - div x y) &lt;= - y)">
<goal name="mod_div_unique.0.1.1.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.68"/></proof>
</goal>
<goal name="mod_div_unique.0.1.1.0.1" expl="false case (true case)" proved="true">
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="mod_div_unique.1.1.0.1" expl="false case (true case)" proved="true">
<proof prover="7"><result status="valid" time="0.01"/></proof>
<goal name="mod_div_unique.0.1.1.1" expl="false case" proved="true">
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="mod_div_unique.1.1.1" expl="false case" proved="true">
<proof prover="7"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
......
......@@ -3,6 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../euler011.mlw" proved="true">
<theory name="ProductFour" proved="true">
<goal name="WP_parameter right_diag_c" expl="VC for right_diag_c" proved="true">
......@@ -1883,31 +1884,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter find_max.349" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter find_max.349.0" expl="assertion" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="WP_parameter find_max.349.0.0" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="WP_parameter find_max.349.0.0.0" expl="assertion" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter find_max.349.0.0.0.0" expl="assertion" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="WP_parameter find_max.349.0.0.0.0.0" expl="assertion" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="WP_parameter find_max.349.0.0.0.0.0.0" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="187"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter find_max.350" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="1.89" steps="3455"/></proof>
......
This diff is collapsed.
......@@ -62,29 +62,6 @@
</goal>
<goal name="inversion_mem_star_gen" proved="true">
<proof prover="8" edited="residual_Residuals_inversion_mem_star_gen_1.v"><result status="valid" time="0.28"/></proof>
<transf name="induction_arg_pr" proved="true" arg1="H2">
<goal name="inversion_mem_star_gen.0" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.1" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.2" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.3" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.4" proved="true">
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="inversion_mem_star_gen.5" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="inversion_mem_star_gen.6" proved="true">
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
<transf name="induction_pr" proved="true" >
<goal name="inversion_mem_star_gen.0" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
......@@ -108,6 +85,33 @@
<proof prover="6"><result status="valid" time="0.17"/></proof>
</goal>
</transf>
<transf name="introduce_premises" proved="true" >
<goal name="inversion_mem_star_gen.0" proved="true">
<transf name="induction_arg_pr" proved="true" arg1="H2">
<goal name="inversion_mem_star_gen.0.0" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.1" proved="true">
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.2" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.3" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.4" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.5" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inversion_mem_star_gen.0.6" proved="true">
<proof prover="5"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="inversion_mem_star" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
......
......@@ -9,25 +9,33 @@
<file name="../sumrange.mlw" proved="true">
<theory name="ArraySum" proved="true">
<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])">
<transf name="introduce_premises" proved="true" >
<goal name="sum_right.0" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_right.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sum_right.0.1" expl="recursive case" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="(x - 1)">
<goal name="sum_right.0.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
<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.0" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="sum_right.0.0.0" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_right.0.0.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sum_right.0.0.0.1" expl="recursive case" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="(x - 1)">
<goal name="sum_right.0.0.0.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="sum_right.1" proved="true">
<transf name="instantiate" proved="true" arg1="h" arg2="(j-i)">
<goal name="sum_right.1.0" proved="true">
<proof prover="2"><result status="valid" time="0.09"/></proof>
<goal name="sum_right.0.1" proved="true">
<transf name="instantiate" proved="true" arg1="h" arg2="(j-i)">
<goal name="sum_right.0.1.0" proved="true">
<proof prover="2"><result status="valid" time="0.13"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
......@@ -65,57 +73,73 @@
</theory>
<theory name="ExtraLemmas" proved="true">
<goal name="sum_concat" proved="true">
<transf name="induction" proved="true" arg1="k">
<goal name="sum_concat.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sum_concat.1" expl="recursive case" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="k">
<goal name="sum_concat.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="sum_concat.0" proved="true">
<transf name="induction" proved="true" arg1="k">
<goal name="sum_concat.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="sum_concat.0.1" expl="recursive case" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="k">
<goal name="sum_concat.0.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="sum_frame" proved="true">
<transf name="assert" proved="true" arg1="(forall x. 0 &lt;= x &lt;= j-i -&gt; sum a1 (j-x) j = sum a2 (j-x) j)">
<transf name="introduce_premises" proved="true" >
<goal name="sum_frame.0" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_frame.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sum_frame.0.1" expl="recursive case" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="(x - 1)">
<goal name="sum_frame.0.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
<transf name="assert" proved="true" arg1="(forall x. 0 &lt;= x &lt;= j-i -&gt; sum a1 (j-x) j = sum a2 (j-x) j)">
<goal name="sum_frame.0.0" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="sum_frame.0.0.0" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_frame.0.0.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="sum_frame.0.0.0.1" expl="recursive case" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="(x - 1)">
<goal name="sum_frame.0.0.0.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="sum_frame.1" proved="true">
<transf name="instantiate" proved="true" arg1="h" arg2="(j-i)">
<goal name="sum_frame.1.0" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<goal name="sum_frame.0.1" proved="true">
<transf name="instantiate" proved="true" arg1="h" arg2="(j-i)">
<goal name="sum_frame.0.1.0" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="sum_update" proved="true">
<transf name="induction" proved="true" arg1="h" arg2="from" arg3="i+1">
<goal name="sum_update.0" expl="base case" proved="true">
<transf name="compute_in_goal" proved="true" >
<transf name="introduce_premises" proved="true" >
<goal name="sum_update.0" proved="true">
<transf name="induction" proved="true" arg1="h" arg2="from" arg3="i+1">
<goal name="sum_update.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
<transf name="compute_in_goal" proved="true" >
<goal name="sum_update.0.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="sum_update.1" expl="recursive case" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="sum_update.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.04"/></proof>
<goal name="sum_update.0.1" expl="recursive case" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="sum_update.0.1.0" expl="recursive case" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
......
......@@ -146,15 +146,19 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter pop.5.6" expl="VC for pop" proved="true">
<transf name="destruct" proved="true" arg1="H">
<transf name="introduce_premises" proved="true" >
<goal name="WP_parameter pop.5.6.0" expl="VC for pop" proved="true">
<transf name="destruct" proved="true" arg1="H">
<goal name="WP_parameter pop.5.6.0.0" expl="VC for pop" proved="true">
<transf name="destruct" proved="true" arg1="H">
<goal name="WP_parameter pop.5.6.0.0.0" expl="VC for pop" proved="true">
<transf name="instantiate" proved="true" arg1="H" arg2="i+1">
<transf name="destruct" proved="true" arg1="H">
<goal name="WP_parameter pop.5.6.0.0.0.0" expl="VC for pop" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<transf name="instantiate" proved="true" arg1="H" arg2="i+1">
<goal name="WP_parameter pop.5.6.0.0.0.0.0" expl="VC for pop" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</transf>
</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