Commit 74c1454f authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example: Braun trees

parent a8b8fe36
(** Purely applicative heaps implemented with Braun trees.
Author: Jean-Christophe Filliâtre (CNRS)
*)
module BraunHeaps
use import int.Int
use import bintree.Tree
use export bintree.Size
use export bintree.Occ
type elt
predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
(* [e] is no greater than the root of [t], if any *)
predicate le_root (e: elt) (t: tree elt) = match t with
| Empty -> true
| Node _ x _ -> le e x
end
predicate heap (t: tree elt) = match t with
| Empty -> true
| Node l x r -> le_root x l && heap l && le_root x r && heap r
end
function minimum (tree elt) : elt
axiom minimum_def: forall l x r. minimum (Node l x r) = x
predicate is_minimum (x: elt) (t: tree elt) =
mem x t && forall e. mem e t -> le x e
(* the root is the smallest element *)
let rec lemma root_is_min (t: tree elt) : unit
requires { heap t && 0 < size t }
ensures { is_minimum (minimum t) t }
variant { t }
= match t with
| Empty -> absurd
| Node l _ r ->
if l <> Empty then root_is_min l;
if r <> Empty then root_is_min r
end
predicate inv (t: tree elt) = match t with
| Empty -> true
| Node l _ r -> (size l = size r || size l = size r + 1) && inv l && inv r
end
let empty () : tree elt
ensures { heap result }
ensures { inv result }
ensures { size result = 0 }
ensures { forall e. not (mem e result) }
= Empty
let is_empty (t: tree elt) : bool
ensures { result <-> size t = 0 }
=
t = Empty
let size (t: tree elt) : int
ensures { result = size t }
=
size t
let get_min (t: tree elt) : elt
requires { heap t && 0 < size t }
ensures { result = minimum t }
=
match t with
| Empty -> absurd
| Node _ x _ -> x
end
let rec add (x: elt) (t: tree elt) : tree elt
requires { heap t }
requires { inv t }
variant { t }
ensures { heap result }
ensures { inv result }
ensures { occ x result = occ x t + 1 }
ensures { forall e. e <> x -> occ e result = occ e t }
ensures { size result = size t + 1 }
=
match t with
| Empty ->
Node Empty x Empty
| Node l y r ->
if le x y then
Node (add y r) x l
else
Node (add x r) y l
end
let rec extract (t: tree elt) : (elt, tree elt)
requires { heap t }
requires { inv t }
requires { 0 < size t }
variant { t }
ensures { let (e, t') = result in
heap t' && inv t' && size t' = size t - 1 &&
occ e t' = occ e t - 1 &&
forall x. x <> e -> occ x t' = occ x t }
=
match t with
| Empty ->
absurd
| Node Empty y r ->
assert { r = Empty };
(y, Empty)
| Node l y r ->
let (x, l) = extract l in
(x, Node r y l)
end
let rec replace_min (x: elt) (t: tree elt)
requires { heap t }
requires { inv t }
requires { 0 < size t }
variant { t }
ensures { heap result }
ensures { inv result }
ensures { if x = minimum t then occ x result = occ x t
else occ x result = occ x t + 1 &&
occ (minimum t) result = occ (minimum t) t - 1 }
ensures { forall e. e <> x -> e <> minimum t -> occ e result = occ e t }
ensures { size result = size t }
=
match t with
| Node l _ r ->
if le_root x l && le_root x r then
Node l x r
else
let lx = get_min l in
if le_root lx r then
(* lx <= x, rx necessarily *)
Node (replace_min x l) lx r
else
(* rx <= x, lx necessarily *)
Node l (get_min r) (replace_min x r)
| Empty ->
absurd
end
let rec merge (l r: tree elt) : tree elt
requires { heap l && heap r }
requires { inv l && inv r }
requires { size r <= size l <= size r + 1 }
ensures { heap result }
ensures { inv result }
ensures { forall e. occ e result = occ e l + occ e r }
ensures { size result = size l + size r }
variant { size l + size r }
=
match l, r with
| _, Empty ->
l
| Node ll lx lr, Node _ ly _ ->
if le lx ly then
Node r lx (merge ll lr)
else
let (x, l) = extract l in
Node (replace_min x r) ly l
| Empty, _ ->
absurd
end
let remove_min (t: tree elt) : tree elt
requires { heap t }
requires { inv t }
requires { 0 < size t }
ensures { heap result }
ensures { inv result }
ensures { occ (minimum t) result = occ (minimum t) t - 1 }
ensures { forall e. e <> minimum t -> occ e result = occ e t }
ensures { size result = size t - 1 }
=
match t with
| Empty -> absurd
| Node l _ r -> merge l r
end
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="../braun_trees.mlw" expanded="true">
<theory name="BraunHeaps" sum="2db2041a3c76fd9d11845d600178cb1a" 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>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter is_empty" expl="VC for is_empty">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter size" expl="VC for size">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter get_min" expl="VC for get_min">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add">
<transf name="split_goal_wp">
<goal name="WP_parameter add.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter add.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter add.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter add.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter add.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter add.6" expl="6. variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter add.7" expl="7. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter add.8" expl="8. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter add.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="WP_parameter add.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter add.11" expl="11. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter add.12" expl="12. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter add.13" expl="13. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter add.14" expl="14. variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter add.15" expl="15. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter add.16" expl="16. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter add.17" expl="17. postcondition">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter add.18" expl="18. postcondition">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter add.19" expl="19. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter add.20" expl="20. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter add.21" expl="21. postcondition">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter extract" expl="VC for extract">
<transf name="split_goal_wp">
<goal name="WP_parameter extract.1" expl="1. unreachable point">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter extract.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter extract.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter extract.4" expl="4. variant decrease">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter extract.5" expl="5. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter extract.6" expl="6. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter extract.7" expl="7. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter extract.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.62"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter replace_min" expl="VC for replace_min">
<transf name="split_goal_wp">
<goal name="WP_parameter replace_min.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter replace_min.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter replace_min.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter replace_min.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter replace_min.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter replace_min.6" expl="6. precondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter replace_min.7" expl="7. variant decrease">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter replace_min.8" expl="8. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter replace_min.9" expl="9. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter replace_min.10" expl="10. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter replace_min.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="WP_parameter replace_min.12" expl="12. postcondition">
<proof prover="1"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="WP_parameter replace_min.13" expl="13. postcondition">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter replace_min.14" expl="14. postcondition">
<proof prover="1"><result status="valid" time="0.83"/></proof>
</goal>
<goal name="WP_parameter replace_min.15" expl="15. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter replace_min.16" expl="16. variant decrease">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter replace_min.17" expl="17. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter replace_min.18" expl="18. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter replace_min.19" expl="19. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter replace_min.20" expl="20. precondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter replace_min.21" expl="21. postcondition">
<proof prover="0"><result status="valid" time="0.61"/></proof>
</goal>
<goal name="WP_parameter replace_min.22" expl="22. postcondition">
<proof prover="1"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="WP_parameter replace_min.23" expl="23. postcondition">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter replace_min.24" expl="24. postcondition">
<proof prover="1"><result status="valid" time="0.60"/></proof>
</goal>
<goal name="WP_parameter replace_min.25" expl="25. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter replace_min.26" expl="26. unreachable point">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</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.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.9" expl="9. variant decrease">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.10" expl="10. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.11" expl="11. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.12" expl="12. precondition">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter merge.13" expl="13. postcondition">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter merge.14" expl="14. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.15" expl="15. postcondition">
<proof prover="1"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="WP_parameter merge.16" expl="16. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter merge.17" expl="17. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.18" expl="18. precondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.19" expl="19. precondition">
<proof prover="1"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter merge.20" expl="20. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.21" expl="21. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter merge.22" expl="22. precondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter merge.23" expl="23. postcondition">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter merge.24" expl="24. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.25" expl="25. postcondition">
<proof prover="1"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="WP_parameter merge.26" expl="26. postcondition">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter merge.27" expl="27. unreachable point">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter remove_min" expl="VC for remove_min">
<proof prover="1"><result status="valid" time="0.03"/></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