gallery: Braun trees have a logarithmic height

parent 430d462c
......@@ -184,4 +184,36 @@ module BraunHeaps
| Node l _ r -> merge l r
end
(** A Braun tree has a logarithmic height *)
use import bintree.Height
use import int.Power
let rec lemma size_height (t1 t2: tree elt)
requires { inv t1 && inv t2 }
variant { size t1 + size t2 }
ensures { size t1 >= size t2 -> height t1 >= height t2 }
= match t1, t2 with
| Node l1 _ r1, Node l2 _ r2 ->
size_height l1 l2;
size_height r1 r2
| _ ->
()
end
let rec lemma inv_height (t: tree elt)
requires { inv t }
variant { t }
ensures { size t > 0 ->
let h = height t in power 2 (h-1) <= size t < power 2 h }
= match t with
| Empty | Node Empty _ _ ->
()
| Node l _ r ->
let h = height t in
assert { height l = h-1 };
inv_height l;
inv_height r
end
end
......@@ -5,7 +5,7 @@
<prover id="0" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<file name="../braun_trees.mlw" expanded="true">
<theory name="BraunHeaps" sum="2db2041a3c76fd9d11845d600178cb1a" expanded="true">
<theory name="BraunHeaps" sum="2df18157743aa6710edbc84397625ded" expanded="true">
<goal name="WP_parameter root_is_min" expl="VC for root_is_min">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
......@@ -198,8 +198,8 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter merge" expl="VC for merge" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter merge" expl="VC for merge">
<transf name="split_goal_wp">
<goal name="WP_parameter merge.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -286,6 +286,59 @@
<goal name="WP_parameter remove_min" expl="VC for remove_min">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter size_height" expl="VC for size_height">
<transf name="split_goal_wp">
<goal name="WP_parameter size_height.1" expl="1. variant decrease">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter size_height.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter size_height.3" expl="3. variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter size_height.4" expl="4. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter size_height.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.67"/></proof>
</goal>
<goal name="WP_parameter size_height.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter size_height.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter inv_height" expl="VC for inv_height">
<transf name="split_goal_wp">
<goal name="WP_parameter inv_height.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter inv_height.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.59"/></proof>
</goal>
<goal name="WP_parameter inv_height.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="WP_parameter inv_height.4" expl="4. variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter inv_height.5" expl="5. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter inv_height.6" expl="6. variant decrease">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter inv_height.7" expl="7. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter inv_height.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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