Commit 2d0eb69b authored by Mario Pereira's avatar Mario Pereira

New examples: leftist heaps, pairing heaps and pairing heaps encoded as binary trees

parent 6825c8fc
module Heap
use import int.Int
type elt
predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
type heap
function size heap : int
function occ elt heap : int
predicate mem (x: elt) (h: heap) = occ x h > 0
function minimum heap : elt
predicate is_minimum (x: elt) (h: heap) =
mem x h && forall e. mem e h -> le x e
axiom min_def:
forall h. 0 < size h -> is_minimum (minimum h) h
val empty () : heap
ensures { size result = 0 }
ensures { forall x. occ x result = 0 }
val is_empty (h: heap) : bool
ensures { result <-> size h = 0 }
val size (h: heap) : int
ensures { result = size h }
val merge (h1 h2: heap) : heap
ensures { forall x. occ x result = occ x h1 + occ x h2 }
ensures { size result = size h1 + size h2 }
val insert (x: elt) (h: heap) : heap
ensures { occ x result = occ x h + 1 }
ensures { forall y. y <> x -> occ y h = occ y result }
ensures { size result = size h + 1 }
val find_min (h: heap) : elt
requires { size h > 0 }
ensures { result = minimum h }
val delete_min (h: heap) : heap
requires { size h > 0 }
ensures { let x = minimum h in occ x result = occ x h - 1 }
ensures { forall y. y <> minimum h -> occ y result = occ y h }
ensures { size result = size h - 1 }
end
module TreeRank
type tree 'a = E | N int (tree 'a) 'a (tree 'a)
end
module Size
use import TreeRank
use import int.Int
function size (t: tree 'a) : int = match t with
| E -> 0
| N _ l _ r -> 1 + size l + size r
end
lemma size_nonneg: forall t: tree 'a. 0 <= size t
lemma size_empty: forall t: tree 'a. 0 = size t <-> t = E
end
module Occ
use import TreeRank
use import int.Int
function occ (x: 'a) (t: tree 'a) : int = match t with
| E -> 0
| N _ l e r -> (if x = e then 1 else 0) + occ x l + occ x r
end
lemma occ_nonneg:
forall x:'a, t. 0 <= occ x t
predicate mem (x: 'a) (t: tree 'a) =
0 < occ x t
end
module LeftistHeap
type elt
predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
use import TreeRank
use export Size
use export Occ
use import int.Int
use import int.MinMax
type t = tree elt
(* [e] is no greater than the root of [h], if any *)
predicate le_root (e: elt) (h: t) = match h with
| E -> true
| N _ _ x _ -> le e x
end
lemma le_root_trans:
forall x y h. le x y -> le_root y h -> le_root x h
(* [h] is a heap *)
predicate is_heap (h: t) = match h with
| E -> true
| N _ l x r -> le_root x l && is_heap l && le_root x r && is_heap r
end
function minimum t : elt
axiom minimum_def: forall l x r s. minimum (N s l x r) = x
predicate is_minimum (x: elt) (h: t) =
mem x h && forall e. mem e h -> le x e
let rec lemma root_is_miminum (h: t) : unit
requires { is_heap h && 0 < size h }
ensures { is_minimum (minimum h) h }
variant { h }
= match h with
| E -> absurd
| N _ l _ r ->
if l <> E then root_is_miminum l;
if r <> E then root_is_miminum r
end
function rank (h: t) : int = match h with
| E -> 0
| N _ l _ r -> 1 + min (rank l) (rank r)
end
predicate leftist (h: t) = match h with
| E -> true
| N s l _ r ->
s = rank h &&
leftist l && leftist r &&
rank l >= rank r
end
predicate leftist_heap (h: t) =
is_heap h && leftist h
let empty () : t
ensures { size result = 0 }
ensures { forall x. occ x result = 0 }
ensures { leftist_heap result }
= E
let is_empty (h: t) : bool
ensures { result <-> size h = 0 }
= h = E
let size (h: t) : int
ensures { result = size h }
= size h
let rank (h: t) : int
requires { leftist_heap h }
ensures { result = rank h }
= match h with
| E -> 0
| N r _ _ _ -> r
end
let make_n (x: elt) (l r: t) : t
requires { leftist_heap r && leftist_heap l }
requires { le_root x l && le_root x r }
ensures { leftist_heap result }
ensures { minimum result = x }
ensures { size result = 1 + size l + size r }
ensures { occ x result = 1 + occ x l + occ x r }
ensures { forall y. x <> y -> occ y result = occ y l + occ y r }
= if rank l >= rank r then N (rank r + 1) l x r
else N (rank l + 1) r x l
let rec merge (h1 h2: t) : t
requires { leftist_heap h1 && leftist_heap h2 }
ensures { size result = size h1 + size h2 }
ensures { forall x. occ x result = occ x h1 + occ x h2 }
ensures { leftist_heap result }
variant { size h1 + size h2 }
= match h1, h2 with
| h, E | E, h -> h
| N _ l1 x1 r1, N _ l2 x2 r2 ->
if le x1 x2 then make_n x1 l1 (merge r1 h2)
else make_n x2 l2 (merge h1 r2)
end
let insert (x: elt) (h: t) : t
requires { leftist_heap h }
ensures { leftist_heap result }
ensures { occ x result = occ x h + 1 }
ensures { forall y. x <> y -> occ y result = occ y h }
ensures { size result = size h + 1 }
= merge (N 1 E x E) h
let find_min (h: t) : elt
requires { leftist_heap h }
requires { 0 < size h }
ensures { result = minimum h }
= match h with
| E -> absurd
| N _ _ x _ -> x
end
let delete_min (h: t) : t
requires { 0 < size h }
requires { leftist_heap h }
ensures { occ (minimum h) result = occ (minimum h) h - 1 }
ensures { forall x. x <> minimum h -> occ x result = occ x h }
ensures { size result = size h - 1 }
ensures { leftist_heap result }
= match h with
| E -> absurd
| N _ 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="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../leftist_heap.mlw" expanded="true">
<theory name="Heap" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="TreeRank" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Size" sum="6f414cd8c85262f7a883e226a4add0bb">
<goal name="size_nonneg">
<transf name="induction_ty_lex">
<goal name="size_nonneg.1" expl="1.">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
</transf>
</goal>
<goal name="size_empty">
<transf name="induction_ty_lex">
<goal name="size_empty.1" expl="1.">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Occ" sum="86544f99c8754e786af5d51f9f25891d" expanded="true">
<goal name="occ_nonneg" expanded="true">
<transf name="induction_ty_lex" expanded="true">
<goal name="occ_nonneg.1" expl="1.">
<proof prover="1"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="LeftistHeap" sum="58ee1098b455dc82539ced85085de45b" expanded="true">
<goal name="le_root_trans">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter root_is_miminum" expl="VC for root_is_miminum" expanded="true">
<proof prover="0"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter is_empty" expl="VC for is_empty">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter size" expl="VC for size">
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter rank" expl="VC for rank">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter make_n" expl="VC for make_n">
<proof prover="1"><result status="valid" time="0.21" steps="819"/></proof>
</goal>
<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" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter merge.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter merge.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal>
<goal name="WP_parameter merge.9" expl="9. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter merge.10" expl="10. variant decrease">
<proof prover="1"><result status="valid" time="0.03" steps="65"/></proof>
</goal>
<goal name="WP_parameter merge.11" expl="11. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="WP_parameter merge.12" expl="12. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="WP_parameter merge.13" expl="13. precondition">
<proof prover="0"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="WP_parameter merge.14" expl="14. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="WP_parameter merge.15" expl="15. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="46"/></proof>
</goal>
<goal name="WP_parameter merge.16" expl="16. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="16"/></proof>
</goal>
<goal name="WP_parameter merge.17" expl="17. variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="66"/></proof>
</goal>
<goal name="WP_parameter merge.18" expl="18. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="58"/></proof>
</goal>
<goal name="WP_parameter merge.19" expl="19. precondition">
<proof prover="1"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="WP_parameter merge.20" expl="20. precondition">
<proof prover="0"><result status="valid" time="0.64"/></proof>
</goal>
<goal name="WP_parameter merge.21" expl="21. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="WP_parameter merge.22" expl="22. postcondition">
<proof prover="1"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="WP_parameter merge.23" expl="23. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter insert" expl="VC for insert">
<proof prover="1"><result status="valid" time="0.04" steps="124"/></proof>
</goal>
<goal name="WP_parameter find_min" expl="VC for find_min">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter delete_min" expl="VC for delete_min">
<proof prover="1"><result status="valid" time="0.03" steps="126"/></proof>
</goal>
</theory>
</file>
</why3session>
module Heap
use import int.Int
type elt
predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
type heap
function size heap : int
function occ elt heap : int
predicate mem (x: elt) (h: heap) = occ x h > 0
function minimum heap : elt
predicate is_minimum (x: elt) (h: heap) =
mem x h && forall e. mem e h -> le x e
axiom min_def:
forall h. 0 < size h -> is_minimum (minimum h) h
val empty () : heap
ensures { size result = 0 }
ensures { forall x. occ x result = 0 }
val is_empty (h: heap) : bool
ensures { result <-> size h = 0 }
val size (h: heap) : int
ensures { result = size h }
val merge (h1 h2: heap) : heap
ensures { forall x. occ x result = occ x h1 + occ x h2 }
ensures { size result = size h1 + size h2 }
val insert (x: elt) (h: heap) : heap
ensures { occ x result = occ x h + 1 }
ensures { forall y. y <> x -> occ y h = occ y result }
ensures { size result = size h + 1 }
val find_min (h: heap) : elt
requires { size h > 0 }
ensures { result = minimum h }
val delete_min (h: heap) : heap
requires { size h > 0 }
ensures { let x = minimum h in occ x result = occ x h - 1 }
ensures { forall y. y <> minimum h -> occ y result = occ y h }
ensures { size result = size h - 1 }
end
module HeapType
use import list.List
type elt
type heap = E | T elt (list heap)
end
module Size
use import HeapType
use import int.Int
use import list.List
function size (h: heap) : int = match h with
| E -> 0
| T _ l -> 1 + size_list l
end
with size_list (l: list heap) : int = match l with
| Nil -> 0
| Cons h r -> size h + size_list r
end
let rec lemma size_nonneg (h: heap)
ensures { size h >= 0 }
variant { h }
= match h with
| E -> ()
| T _ l -> size_list_nonneg l
end
with size_list_nonneg (l: list heap)
ensures { size_list l >= 0 }
variant { l }
= match l with
| Nil -> ()
| Cons h r ->
size_nonneg h; size_list_nonneg r
end
let lemma size_empty (h: heap)
ensures { size h = 0 <-> h = E }
= match h with
| E -> ()
| T _ l ->
size_list_nonneg l
end
end
module Occ
use import HeapType
use import int.Int
use import list.List
function occ (x: elt) (h: heap) : int = match h with
| E -> 0
| T e l -> (if x = e then 1 else 0) + occ_list x l
end
with occ_list (x: elt) (l: list heap) : int = match l with
| Nil -> 0
| Cons h r -> occ x h + occ_list x r
end
let rec lemma occ_nonneg (x: elt) (h: heap)
ensures { occ x h >= 0 }
variant { h }
= match h with
| E -> ()
| T _ l -> occ_list_nonneg x l
end
with occ_list_nonneg (x: elt) (l: list heap)
ensures { occ_list x l >= 0 }
variant { l }
= match l with
| Nil -> ()
| Cons h r ->
occ_nonneg x h; occ_list_nonneg x r
end
predicate mem (x: elt) (h: heap) =
0 < occ x h
predicate mem_list (x: elt) (l: list heap) =
0 < occ_list x l
end
module PairingHeap
use import int.Int
use export HeapType
use export Size
use export Occ
use import list.List
use import list.Length
predicate le elt elt
clone import relations.TotalPreOrder with type t = elt, predicate rel = le
(* [e] is no greater than the root of [h], if any *)
predicate le_root (e: elt) (h: heap) = match h with
| E -> true
| T x _ -> le e x
end
lemma le_root_trans:
forall x y h. le x y -> le_root y h -> le_root x h
(* [e] is no greater than the roots of the trees in [l] *)
predicate le_roots (e: elt) (l: list heap) = match l with
| Nil -> true
| Cons h r -> le_root e h && le_roots e r
end
lemma le_roots_trans:
forall x y l. le x y -> le_roots y l -> le_roots x l
predicate no_middle_empty (h: heap) = match h with
| E -> true
| T _ l -> no_middle_empty_list l
end
with no_middle_empty_list (l: list heap) = match l with
| Nil -> true
| Cons h r -> h <> E && no_middle_empty h && no_middle_empty_list r
end
predicate heap (h: heap) = match h with
| E -> true
| T x l -> le_roots x l && heaps l
end
with heaps (l: list heap) = match l with
| Nil -> true
| Cons h r -> heap h && heaps r
end
predicate inv (h: heap) =
heap h && no_middle_empty h
let rec lemma heap_mem (h: heap)
requires { heap h }
variant { h }
ensures { forall x. le_root x h -> forall y. mem y h -> le x y }
= match h with
| E -> ()
| T _ l -> heap_mem_list l
end
with heap_mem_list (l: list heap)
requires { heaps l }
variant { l }
ensures { forall x. le_roots x l -> forall y. mem_list y l -> le x y }
= match l with
| Nil -> ()
| Cons h r ->
heap_mem h;
heap_mem_list r
end
predicate is_minimum (x: elt) (h: heap) =
mem x h && forall e. mem e h -> le x e
function minimum heap : elt
axiom minimum_def: forall x l. minimum (T x l) = x
let lemma root_is_minimum (h: heap)
requires { 0 < size h }
requires { heap h }
ensures { is_minimum (minimum h) h }
= match h with
| E -> absurd
| T x l -> occ_list_nonneg x l
end
let empty () : heap
ensures { inv result }
ensures { size result = 0 }
ensures { forall e. not (mem e result) }
= E
let is_empty (h: heap) : bool
ensures { result <-> size h = 0 }
= h = E
let merge (h1 h2: heap) : heap
requires { inv h1 && inv h2 }
ensures { inv result }
ensures { size result = size h1 + size h2 }
ensures { forall x. occ x result = occ x h1 + occ x h2 }
= match h1, h2 with
| E, h | h, E -> h
| T x1 l1, T x2 l2 ->
if le x1 x2 then
T x1 (Cons h2 l1)
else
T x2 (Cons h1 l2)
end
let insert (x: elt) (h: heap) : heap
requires { inv h }
ensures { inv result }
ensures { size result = size h + 1 }
ensures { occ x result = occ x h + 1 }
ensures { forall y. x <> y -> occ y result = occ y h }
= merge (T x Nil) h
let find_min (h: heap) : elt
requires { 0 < size h }
requires { inv h }
ensures { result = minimum h }
= match h with
| E -> absurd
| T x _ -> x
end
let rec merge_pairs (l: list heap) : heap
requires { heaps l && no_middle_empty_list l }
ensures { inv result }
ensures { size result = size_list l }
ensures { forall x. occ x result = occ_list x l }
variant { length l }
= match l with
| Nil -> E
| Cons h Nil -> assert { h <> E }; h
| Cons h1 (Cons h2 r) ->
merge (merge h1 h2) (merge_pairs r)
end
let delete_min (h: heap) : heap
requires { inv h }
requires { 0 < size h }