Commit 8ba809cb by Jean-Christophe Filliâtre

### new example (wip): binomial heaps

parent 717862a9
 (** Binomial heaps. Author: Jean-Christophe Filliâtre (CNRS) *) module BinomialHeap use import int.Int use import list.List use import list.Length use import list.Reverse type elt predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le type tree = { elem: elt; children: list tree; } (* [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 e t.elem && le_roots e r end lemma le_roots_trans: forall x y l. le x y -> le_roots y l -> le_roots x l (* [l] is a list of heaps *) predicate heaps (l: list tree) = match l with | Nil -> true | Cons {elem=e; children=c} r -> le_roots e c && heaps c && heaps r end lemma heaps_reverse: forall h. heaps h -> heaps (reverse h) function rank (t: tree) : int = length t.children function link (t1 t2: tree) : tree = if le t1.elem t2.elem then { t1 with children = Cons t2 t1.children } else { t2 with children = Cons t1 t2.children } (* predicate mem (x: elt) (l: list tree) = *) (* match l with *) (* | Nil -> false *) (* | Cons { elem = y; children = c } r -> x = y || mem x c || mem x r *) (* end *) function occ (x: elt) (l: list tree) : int = match l with | Nil -> 0 | Cons { elem = y; children = c } r -> (if x = y then 1 else 0) + occ x c + occ x r end lemma occ_nonneg: forall x l. 0 <= occ x l (* let rec lemma occ_nonneg (x: elt) (l: list tree) variant { l } ensures { 0 <= occ x l } = match l with | Nil -> () | Cons { elem = y; children = c } r -> occ_nonneg x c; occ_nonneg x r end *) lemma occ_reverse: forall x l. occ x l = occ x (reverse l) predicate mem (x: elt) (l: list tree) = occ x l > 0 lemma heaps_mem: forall x l. le_roots x l -> forall y. mem y l -> le x y predicate has_order (k: int) (l: list tree) = match l with | Nil -> k = 0 | Cons { children = c } r -> has_order (k-1) c && has_order (k-1) r end function size (l: list tree) : int = match l with | Nil -> 0 | Cons { children = c } r -> 1 + size c + size r end (* a binomial heap is a list of trees *) type heap = list tree (* predicate inv (t: t) = match t with | Empty -> true | Node l _ r -> (size l = size r || size l = size r + 1) && inv l && inv r end *) let empty () : heap ensures { heaps result } (* ensures { inv result } *) (* ensures { size result = 0 } *) ensures { forall e. not (mem e result) } = Nil (* function minimum (list tree) : elt axiom minimum_def: forall l x r. minimum (Node l x r) = x predicate is_minimum (x: elt) (l: list tree) = mem x t && forall e. mem e t -> le x e *) (* let is_empty (h: heap) : bool ensures { result <-> size h = 0 } = h = Nil *) let get_min (h: heap) : elt requires { heaps h } (* requires { 0 < size h } *) requires { h <> Nil } ensures { mem result h } ensures { forall x. mem x h -> le result x } = match h with | Nil -> absurd | Cons t l -> let rec aux (m: elt) (l: list tree) : elt requires { heaps l } variant { l } ensures { result = m || mem result l } ensures { le result m } ensures { forall x. mem x l -> le result x } = match l with | Nil -> m | Cons {elem=x} r -> aux (if le x m then x else m) r end in aux t.elem l end let rec add_tree (t: tree) (h: heap) requires { heaps (Cons t Nil) } requires { heaps h } variant { h } ensures { heaps result } ensures { forall x. occ x result = occ x (Cons t Nil) + occ x h } = match h with | Nil -> Cons t Nil | Cons hd tl -> if rank t < rank hd then Cons t h else if rank t = rank hd then add_tree (link t hd) tl else (* this case will never be used with usual binomial heaps *) Cons hd (add_tree t tl) end let add (x: elt) (h: heap) : heap requires { heaps h } (* requires { inv t } *) ensures { heaps result } (* ensures { inv result } *) ensures { occ x result = occ x h + 1 } ensures { forall e. e <> x -> occ e result = occ e h } (* ensures { size result = size h + 1 } *) = add_tree { elem = x; children = Nil } h let rec merge (h1 h2: heap) requires { heaps h1 } requires { heaps h2 } variant { h2 } ensures { heaps result } ensures { forall x. occ x result = occ x h1 + occ x h2 } = match h2 with | Nil -> h1 | Cons hd2 tl2 -> merge (add_tree hd2 h1) tl2 end let rec extract_min_tree (h: heap) : (tree, heap) requires { heaps h } (* requires { 0 < size h } *) requires { h <> Nil } variant { h } ensures { let (t, h') = result in heaps (Cons t Nil) && heaps h' && le_roots t.elem h && (* inv t' && size h' = size h - 1 && *) forall x. occ x h = occ x (Cons t Nil) + occ x h' } = match h with | Nil -> absurd | Cons t Nil -> (t, Nil) | Cons t tl -> let (t', tl') = extract_min_tree tl in if le t.elem t'.elem then (t, tl) else (t', Cons t tl') end let rec extract_min (h: heap) : (elt, heap) requires { heaps h } (* requires { inv h } *) (* requires { 0 < size h } *) requires { h <> Nil } variant { h } ensures { let (e, h') = result in heaps h' && (* inv t' && size h' = size h - 1 && *) occ e h' = occ e h - 1 && forall x. x <> e -> occ x h' = occ x h } = let (t, h') = extract_min_tree h in (t.elem, merge (reverse t.children) h') end
This diff is collapsed.