new example: tree_of_list

parent ab1d9167
(** Build a tree of logarithmic height from a list, in linear time,
while preserving the order of elements
Author: Jean-Christophe Filliâtre (CNRS)
*)
module TreeOfList
use import int.Int
use import int.ComputerDivision
use import int.Power
use import list.List
use import list.Append
use import list.Length
use import bintree.Tree
use import bintree.Size
use import bintree.Inorder
use import bintree.InorderLength
use import bintree.Height
type elt
let rec tree_of_list_aux (n: int) (l: list elt) : (tree elt, list elt)
requires { 0 <= n <= length l }
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) }
=
if n = 0 then
(Empty, l)
else
let n = n - 1 in
let n1 = div n 2 in
let (left, l) = tree_of_list_aux n1 l in
match l with
| Nil -> absurd
| Cons x l -> let (right, l) = tree_of_list_aux (n - n1) l in
(Node left x right, l)
end
let tree_of_list (l: list elt) : tree elt
ensures { inorder result = l }
ensures { size result > 0 -> let h = height result in
- power 2 (h-1) <= size result < power 2 h }
=
let (t, l) = tree_of_list_aux (length l) l in
assert { l = Nil };
t
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<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="../tree_of_list.mlw">
<theory name="TreeOfList" sum="a402daaeced35766f5e306330648f95a">
<goal name="WP_parameter tree_of_list_aux" expl="VC for tree_of_list_aux">
<transf name="split_goal_wp">
<goal name="WP_parameter tree_of_list_aux.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.2" expl="2. variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.4" expl="4. unreachable point">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.5" expl="5. variant decrease">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.6" expl="6. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.7" expl="7. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter tree_of_list_aux.7.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.7.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.7.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter tree_of_list_aux.7.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter tree_of_list" expl="VC for tree_of_list">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</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