Commit 489ad728 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

Braun trees: size computed in time O(log^2(n))

algorithm from a paper by Okasaki
Three Algorithms on Braun Trees (Functional Pearl)
JFP 7 (6), 1997
parent 2289299d
(** Purely applicative heaps implemented with Braun trees.
Braun trees are binary trees where, for each node, the left subtree
has the same size of the right subtree or is one element larger
(predicate [inv]).
Consequently, a Braun tree has logarithmic height (lemma [inv_height]).
The nice thing with Braun trees is that we do not need extra information
to ensure logarithmic height.
We also prove an algorithm from Okasaki to compute the size of a braun
tree in time O(log^2(n)) (function [fast_size]).
Author: Jean-Christophe Filliâtre (CNRS)
*)
......@@ -184,6 +195,44 @@ module BraunHeaps
| Node l _ r -> merge l r
end
(** The size of a Braun tree can be computed in time O(log^2(n))
from
Three Algorithms on Braun Trees (Functional Pearl)
Chris Okasaki
J. Functional Programming 7 (6) 661–666, November 1997 *)
use import int.ComputerDivision
let rec diff (m: int) (t: tree elt)
requires { inv t }
requires { 0 <= m <= size t <= m + 1 }
variant { t }
ensures { size t = m + result }
= match t with
| Empty ->
0
| Node l _ r ->
if m = 0 then
1
else if mod m 2 = 1 then
(* m = 2k + 1 *)
diff (div m 2) l
else
(* m = 2k + 2 *)
diff (div (m - 1) 2) r
end
let rec fast_size (t: tree elt) : int
requires { inv t}
variant { t }
ensures { result = size t }
=
match t with
| Empty -> 0
| Node l _ r -> let m = size r in 1 + 2 * m + diff m l
end
(** A Braun tree has a logarithmic height *)
use import bintree.Height
......
......@@ -4,8 +4,8 @@
<why3session shape_version="4">
<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="2df18157743aa6710edbc84397625ded" expanded="true">
<file name="../braun_trees.mlw">
<theory name="BraunHeaps" sum="db95d5e9f116a63bf2d23d3bf802db5f">
<goal name="WP_parameter root_is_min" expl="VC for root_is_min">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
......@@ -286,53 +286,103 @@
<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 diff" expl="VC for diff">
<transf name="split_goal_wp">
<goal name="WP_parameter diff.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="9"/></proof>
</goal>
<goal name="WP_parameter diff.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter diff.3" expl="3. variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="WP_parameter diff.4" expl="4. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter diff.5" expl="5. precondition">
<proof prover="1"><result status="valid" time="0.05" steps="50"/></proof>
</goal>
<goal name="WP_parameter diff.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.07" steps="34"/></proof>
</goal>
<goal name="WP_parameter diff.7" expl="7. variant decrease">
<proof prover="1"><result status="valid" time="0.01" steps="24"/></proof>
</goal>
<goal name="WP_parameter diff.8" expl="8. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter diff.9" expl="9. precondition">
<proof prover="1"><result status="valid" time="0.74" steps="143"/></proof>
</goal>
<goal name="WP_parameter diff.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.80" steps="51"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fast_size" expl="VC for fast_size">
<transf name="split_goal_wp">
<goal name="WP_parameter fast_size.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter fast_size.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter fast_size.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="63"/></proof>
</goal>
<goal name="WP_parameter fast_size.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
</transf>
</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>
<proof prover="1"><result status="valid" time="0.03" steps="79"/></proof>
</goal>
<goal name="WP_parameter size_height.2" expl="2. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="47"/></proof>
</goal>
<goal name="WP_parameter size_height.3" expl="3. variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="WP_parameter size_height.4" expl="4. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
<goal name="WP_parameter size_height.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.67"/></proof>
<proof prover="1"><result status="valid" time="0.67" steps="384"/></proof>
</goal>
<goal name="WP_parameter size_height.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="WP_parameter size_height.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="9"/></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>
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter inv_height.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.59"/></proof>
<proof prover="1"><result status="valid" time="0.59" steps="175"/></proof>
</goal>
<goal name="WP_parameter inv_height.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="0.19"/></proof>
<proof prover="1"><result status="valid" time="0.19" steps="118"/></proof>
</goal>
<goal name="WP_parameter inv_height.4" expl="4. variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="36"/></proof>
</goal>
<goal name="WP_parameter inv_height.5" expl="5. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="31"/></proof>
</goal>
<goal name="WP_parameter inv_height.6" expl="6. variant decrease">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="33"/></proof>
</goal>
<goal name="WP_parameter inv_height.7" expl="7. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="WP_parameter inv_height.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......
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