Wiki Agenda Contact Version française

Pairing heaps

Purely applicative implementation of priority queues using pairing heaps.


Authors: Mário Pereira

Topics: Data Structures

Tools: 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

ObligationsAlt-Ergo 2.3.0
VC for empty0.00

Theory "pairing_heap.Size": fully verified

ObligationsAlt-Ergo 2.3.0
VC for size_nonneg0.00
VC for size_tree_nonneg0.01
VC for size_list_nonneg0.01
VC for size_empty0.00

Theory "pairing_heap.Occ": fully verified

ObligationsAlt-Ergo 2.3.0
VC for occ_nonneg0.00
VC for occ_tree_nonneg0.00
VC for occ_list_nonneg0.01

Theory "pairing_heap.PairingHeap": fully verified

ObligationsAlt-Ergo 2.3.0CVC4 1.7
le_root_trans0.01---
le_roots_trans------
induction_ty_lex
le_roots_trans.00.01---
VC for heap0.01---
VC for heap_mem0.03---
VC for heap_mem_tree0.06---
VC for heap_mem_list0.05---
VC for root_is_minimum------
split_vc
unreachable point0.01---
postcondition0.58---
VC for empty0.01---
VC for is_empty0.01---
VC for merge------
split_vc
precondition0.01---
precondition0.00---
precondition0.01---
precondition0.03---
precondition0.03---
postcondition------
split_vc
postcondition0.00---
postcondition0.00---
postcondition0.00---
postcondition0.01---
postcondition0.01---
postcondition------
split_vc
postcondition0.01---
postcondition0.01---
postcondition0.01---
postcondition0.03---
postcondition0.03---
VC for insert0.04---
VC for find_min0.01---
VC for merge_pairs------
split_vc
precondition0.00---
precondition0.01---
precondition0.01---
precondition0.02---
variant decrease0.01---
precondition0.01---
postcondition------
split_vc
postcondition0.00---
postcondition0.01---
postcondition0.01---
postcondition------
split_vc
postcondition0.03---
postcondition0.01---
postcondition0.02---
VC for delete_min------
split_vc
unreachable point0.01---
precondition0.01---
postcondition------
split_vc
postcondition---0.04
postcondition------
split_vc
postcondition---0.05
postcondition0.50---

Theory "pairing_heap.Correct": fully verified

ObligationsAlt-Ergo 2.3.0
Heap.TotalPreOrder.Refl0.01
Heap.TotalPreOrder.Trans0.01
Heap.TotalPreOrder.Total0.01
Heap.min_def0.01
VC for empty'refn0.01
VC for is_empty'refn0.01
VC for merge'refn0.01
VC for insert'refn0.01
VC for find_min'refn0.01
VC for delete_min'refn0.01