Pairing heaps
Purely applicative implementation of priority queues using pairing heaps.
Auteurs: Mário Pereira
Catégories: Data Structures
Outils: Why3
see also the index (by topic, by tool, by reference, by year)
Pairing heaps (M. Fredman, R. Sedgewick, D. Sleator, R. Tarjan, 1986).
Purely applicative implementation, following Okasaki's implementation in his book "Purely Functional Data Structures" (Section 5.5).
Author: Mário Pereira (Université Paris Sud)
module Heap use int.Int type elt val predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . 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 constant 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 list.List type elt type raw_heap = E | H tree with tree = T elt (list tree) end module Size use HeapType use int.Int use list.List function size_heap (h: raw_heap) : int = match h with | E -> 0 | H t -> size_tree t end with size_tree (t: tree) : int = match t with | T _ l -> 1 + size_list l end with size_list (l: list tree) : int = match l with | Nil -> 0 | Cons t l -> size_tree t + size_list l end let rec lemma size_nonneg (h: raw_heap) ensures { size_heap h >= 0 } variant { h } = match h with | E -> () | H t -> size_tree_nonneg t end with lemma size_tree_nonneg (t: tree) ensures { size_tree t >= 0 } variant { t } = match t with T _ l -> size_list_nonneg l end with lemma size_list_nonneg (l: list tree) ensures { size_list l >= 0 } variant { l } = match l with | Nil -> () | Cons t r -> size_tree_nonneg t; size_list_nonneg r end let lemma size_empty (h: raw_heap) ensures { size_heap h = 0 <-> h = E } = match h with | E -> () | H t -> size_tree_nonneg t end end module Occ use HeapType use int.Int use list.List function occ_heap (x: elt) (h: raw_heap) : int = match h with | E -> 0 | H t -> occ_tree x t end with occ_tree (x: elt) (t: tree) : int = match t with | T e l -> (if x = e then 1 else 0) + occ_list x l end with occ_list (x: elt) (l: list tree) : int = match l with | Nil -> 0 | Cons t r -> occ_tree x t + occ_list x r end let rec lemma occ_nonneg (x: elt) (h: raw_heap) ensures { occ_heap x h >= 0 } variant { h } = match h with | E -> () | H t -> occ_tree_nonneg x t end with lemma occ_tree_nonneg (x: elt) (t: tree) ensures { occ_tree x t >= 0 } variant { t } = match t with T _ l -> occ_list_nonneg x l end with lemma occ_list_nonneg (x: elt) (l: list tree) ensures { occ_list x l >= 0 } variant { l } = match l with | Nil -> () | Cons t r -> occ_tree_nonneg x t; occ_list_nonneg x r end predicate mem (x: elt) (h: raw_heap) = 0 < occ_heap x h predicate mem_tree (x: elt) (t: tree) = 0 < occ_tree x t predicate mem_list (x: elt) (l: list tree) = 0 < occ_list x l end module PairingHeap use int.Int use export HeapType use export Size use export Occ use list.List use list.Length val predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . (* [e] is no greater than the root of [h], if any *) predicate le_tree (e: elt) (t: tree) = match t with | T x _ -> le e x end predicate le_root (e: elt) (h: raw_heap) = match h with | E -> true | H t -> le_tree e t 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 tree) = match l with | Nil -> true | Cons t r -> le_tree e t && 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 heap (h: raw_heap) = match h with | E -> true | H t -> heap_tree t end with heap_tree (t: tree) = match t with | T x l -> le_roots x l && heap_list l end with heap_list (l: list tree) = match l with | Nil -> true | Cons t r -> heap_tree t && heap_list r end type heap = { h: raw_heap } invariant { heap h } by { h = E } function size (hh: heap) : int = size_heap hh.h function occ (e: elt) (hh: heap) : int = occ_heap e hh.h let rec lemma heap_mem (h: raw_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 -> () | H t -> heap_mem_tree t end with heap_mem_tree (t: tree) requires { heap_tree t } variant { t } ensures { forall x. le_tree x t -> forall y. mem_tree y t -> le x y } = match t with T _ l -> heap_mem_list l end with heap_mem_list (l: list tree) requires { heap_list l } variant { l } ensures { forall x. le_roots x l -> forall y. mem_list y l -> le x y } = match l with | Nil -> () | Cons t r -> heap_mem_tree t; heap_mem_list r end predicate is_minimum_tree (x: elt) (t: tree) = mem_tree x t && forall e. mem_tree e t -> le x e predicate is_minimum (x: elt) (h: raw_heap) = mem x h && forall e. mem e h -> le x e function minimum_tree tree : elt axiom minimum_tree_def: forall x l. minimum_tree (T x l) = x function minimum raw_heap : elt axiom minimum_def: forall t. minimum (H t) = minimum_tree t function minimum_heap (hh: heap) : elt = minimum hh.h let lemma root_is_minimum (h: raw_heap) requires { 0 < size_heap h } requires { heap h } ensures { is_minimum (minimum h) h } = match h with | E -> absurd | H (T e l) -> occ_list_nonneg e l end let constant empty : heap = { h = E } ensures { size_heap result.h = 0 } ensures { forall e. not (mem e result.h) } let is_empty (hh: heap) : bool ensures { result <-> size_heap hh.h = 0 } = match hh.h with E -> true | _ -> false end let merge (h1 h2: heap) : heap ensures { size_heap result.h = size_heap h1.h + size_heap h2.h } ensures { forall x. occ_heap x result.h = occ_heap x h1.h + occ_heap x h2.h } = match h1.h, h2.h with | E, h | h, E -> { h = h } | H (T x1 l1), H (T x2 l2) -> if le x1 x2 then { h = H (T x1 (Cons (T x2 l2) l1)) } else { h = H (T x2 (Cons (T x1 l1) l2)) } end let insert (x: elt) (hh: heap) : heap ensures { size_heap result.h = size_heap hh.h + 1 } ensures { occ_heap x result.h = occ_heap x hh.h + 1 } ensures { forall y. x <> y -> occ_heap y result.h = occ_heap y hh.h } = merge { h = H (T x Nil) } hh let find_min (hh: heap) : elt requires { 0 < size_heap hh.h } ensures { result = minimum hh.h } = match hh.h with | E -> absurd | H (T x _) -> x end let rec merge_pairs (l: list tree) : heap requires { heap_list l } ensures { size_heap result.h = size_list l } ensures { forall x. occ_heap x result.h = occ_list x l } variant { length l } = match l with | Nil -> { h = E } | Cons t Nil -> { h = H t } | Cons t1 (Cons t2 r) -> let h1 = { h = H t1 } in let h2 = { h = H t2 } in merge (merge h1 h2) (merge_pairs r) end let delete_min (hh: heap) : heap requires { 0 < size_heap hh.h } ensures { occ_heap (minimum hh.h) result.h = occ_heap (minimum hh.h) hh.h - 1 } ensures { forall y. y <> minimum hh.h -> occ_heap y result.h = occ_heap y hh.h } ensures { size_heap result.h = size_heap hh.h - 1 } = match hh.h with | E -> absurd | H (T _ l) -> merge_pairs l end end module Correct use PairingHeap use Size clone Heap with type elt, type heap, val le, function size, function occ, function minimum = minimum_heap, val empty, val is_empty, val merge, val insert, val find_min, val delete_min end
download ZIP archive
Why3 Proof Results for Project "pairing_heap"
Theory "pairing_heap.Heap": fully verified
Obligations | Alt-Ergo 2.3.0 |
VC for empty | 0.00 |
Theory "pairing_heap.Size": fully verified
Obligations | Alt-Ergo 2.3.0 |
VC for size_nonneg | 0.00 |
VC for size_tree_nonneg | 0.01 |
VC for size_list_nonneg | 0.01 |
VC for size_empty | 0.00 |
Theory "pairing_heap.Occ": fully verified
Obligations | Alt-Ergo 2.3.0 |
VC for occ_nonneg | 0.00 |
VC for occ_tree_nonneg | 0.00 |
VC for occ_list_nonneg | 0.01 |
Theory "pairing_heap.PairingHeap": fully verified
Obligations | Alt-Ergo 2.3.0 | CVC4 1.7 | CVC5 1.0.5 | ||
le_root_trans | 0.01 | --- | --- | ||
le_roots_trans | --- | --- | --- | ||
induction_ty_lex | |||||
le_roots_trans.0 | 0.01 | --- | --- | ||
VC for heap | 0.01 | --- | --- | ||
VC for heap_mem | 0.03 | --- | --- | ||
VC for heap_mem_tree | 0.06 | --- | --- | ||
VC for heap_mem_list | 0.05 | --- | --- | ||
VC for root_is_minimum | --- | --- | --- | ||
split_vc | |||||
unreachable point | 0.01 | --- | --- | ||
postcondition | 0.58 | --- | --- | ||
VC for empty | 0.01 | --- | --- | ||
VC for is_empty | 0.01 | --- | --- | ||
VC for merge | --- | --- | --- | ||
split_vc | |||||
precondition | 0.01 | --- | --- | ||
precondition | 0.00 | --- | --- | ||
precondition | 0.01 | --- | --- | ||
precondition | 0.03 | --- | --- | ||
precondition | 0.03 | --- | --- | ||
postcondition | --- | --- | --- | ||
split_vc | |||||
postcondition | 0.00 | --- | --- | ||
postcondition | 0.00 | --- | --- | ||
postcondition | --- | --- | 0.05 | ||
postcondition | 0.01 | --- | --- | ||
postcondition | --- | --- | --- | ||
split_vc | |||||
postcondition | 0.01 | --- | --- | ||
postcondition | 0.01 | --- | --- | ||
postcondition | --- | --- | 0.06 | ||
postcondition | 0.03 | --- | --- | ||
VC for insert | 0.04 | --- | --- | ||
VC for find_min | 0.01 | --- | --- | ||
VC for merge_pairs | --- | --- | --- | ||
split_vc | |||||
precondition | 0.00 | --- | --- | ||
precondition | 0.01 | --- | --- | ||
precondition | 0.01 | --- | --- | ||
precondition | 0.02 | --- | --- | ||
variant decrease | 0.01 | --- | --- | ||
precondition | 0.01 | --- | --- | ||
postcondition | --- | --- | --- | ||
split_vc | |||||
postcondition | 0.01 | --- | --- | ||
postcondition | 0.00 | --- | --- | ||
postcondition | 0.01 | --- | --- | ||
postcondition | --- | --- | --- | ||
split_vc | |||||
postcondition | 0.03 | --- | --- | ||
postcondition | 0.01 | --- | --- | ||
postcondition | 0.02 | --- | --- | ||
VC for delete_min | --- | --- | --- | ||
split_vc | |||||
unreachable point | 0.01 | --- | --- | ||
precondition | 0.01 | --- | --- | ||
postcondition | --- | --- | --- | ||
split_vc | |||||
postcondition | --- | 0.04 | --- | ||
postcondition | --- | --- | --- | ||
split_vc | |||||
postcondition | --- | 0.05 | --- | ||
postcondition | 0.29 | --- | --- |
Theory "pairing_heap.Correct": fully verified
Obligations | Alt-Ergo 2.3.0 |
Heap.TotalPreOrder.Refl | 0.01 |
Heap.TotalPreOrder.Trans | 0.01 |
Heap.TotalPreOrder.Total | 0.01 |
Heap.min_def | 0.01 |
VC for empty'refn | 0.01 |
VC for is_empty'refn | 0.01 |
VC for merge'refn | 0.01 |
VC for insert'refn | 0.01 |
VC for find_min'refn | 0.01 |
VC for delete_min'refn | 0.01 |