Commit 7d029696 authored by MARCHE Claude's avatar MARCHE Claude

fix broken proof

parent 3e215988
......@@ -26,7 +26,7 @@ module TreeOfList
variant { n }
ensures { let t, l' = result in
inorder t ++ l' = l && size t = n &&
(n> 0 -> let h = height t in power 2 (h-1) <= n < power 2 h) }
(n > 0 -> let h = height t in power 2 (h-1) <= n < power 2 h) }
=
if n = 0 then
Empty, l
......
......@@ -3,13 +3,45 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../tree_of_list.mlw" proved="true">
<theory name="TreeOfList" proved="true">
<goal name="VC tree_of_list_aux" expl="VC for tree_of_list_aux" proved="true">
<proof prover="1"><result status="valid" time="0.73" steps="1456"/></proof>
<transf name="split_vc" proved="true" >
<goal name="VC tree_of_list_aux.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC tree_of_list_aux.1" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC tree_of_list_aux.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC tree_of_list_aux.3" expl="unreachable point" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC tree_of_list_aux.4" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC tree_of_list_aux.5" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="36"/></proof>
</goal>
<goal name="VC tree_of_list_aux.6" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="l&#39;1">
<goal name="VC tree_of_list_aux.6.0" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC tree_of_list_aux.6.1" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.22"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC tree_of_list" expl="VC for tree_of_list" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="108"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="0.02" steps="108"/></proof>
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
</theory>
</file>
......
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