skew_heaps.mlw 3.71 KB
 Jean-Christophe Filliatre committed May 17, 2014 1 2 3 4 `````` module SkewHeaps use import bintree.Tree `````` Jean-Christophe Filliatre committed May 17, 2014 5 6 `````` use export bintree.Size use export bintree.Occ `````` Jean-Christophe Filliatre committed May 17, 2014 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 `````` 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 (* [t] is a heap *) 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 `````` Jean-Christophe Filliatre committed May 17, 2014 25 26 27 `````` function minimum (tree elt) : elt axiom minimum_def: forall l x r. minimum (Node l x r) = x `````` Jean-Christophe Filliatre committed May 17, 2014 28 29 30 31 `````` 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 *) `````` Jean-Christophe Filliatre committed May 17, 2014 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 `````` let rec lemma root_is_min (t: tree elt) : unit requires { heap t && 0 < size t } ensures { is_minimum (minimum t) t } variant { size 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 let empty () : tree elt ensures { heap 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 } `````` Jean-Christophe Filliatre committed May 17, 2014 57 `````` = `````` Jean-Christophe Filliatre committed May 17, 2014 58 `````` size t `````` Jean-Christophe Filliatre committed May 17, 2014 59 60 `````` let get_min (t: tree elt) : elt `````` Jean-Christophe Filliatre committed May 17, 2014 61 62 `````` requires { heap t && 0 < size t } ensures { result = minimum t } `````` Jean-Christophe Filliatre committed May 17, 2014 63 64 65 66 67 68 69 70 71 72 `````` = match t with | Empty -> absurd | Node _ x _ -> x end let rec merge (t1 t2: tree elt) : tree elt requires { heap t1 && heap t2 } ensures { heap result } ensures { forall e. occ e result = occ e t1 + occ e t2 } `````` Jean-Christophe Filliatre committed May 17, 2014 73 `````` ensures { size result = size t1 + size t2 } `````` Jean-Christophe Filliatre committed May 17, 2014 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 `````` variant { size t1 + size t2 } = match t1, t2 with | Empty, _ -> t2 | _, Empty -> t1 | Node l1 x1 r1, Node l2 x2 r2 -> if le x1 x2 then Node (merge r1 t2) x1 l1 else Node (merge r2 t1) x2 l2 end let add (x: elt) (t: tree elt) : tree elt requires { heap t } ensures { heap result } ensures { occ x result = occ x t + 1 } `````` Jean-Christophe Filliatre committed May 17, 2014 90 91 `````` ensures { forall e. e <> x -> occ e result = occ e t } ensures { size result = size t + 1 } `````` Jean-Christophe Filliatre committed May 17, 2014 92 93 94 `````` = merge (Node Empty x Empty) t `````` Jean-Christophe Filliatre committed May 17, 2014 95 96 `````` let remove_min (t: tree elt) : tree elt requires { heap t && 0 < size t } `````` Jean-Christophe Filliatre committed May 17, 2014 97 `````` ensures { heap result } `````` Jean-Christophe Filliatre committed May 17, 2014 98 99 100 `````` 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 } `````` Jean-Christophe Filliatre committed May 17, 2014 101 102 103 104 105 106 107 `````` = match t with | Empty -> absurd | Node l _ r -> merge l r end end `````` Jean-Christophe Filliatre committed May 17, 2014 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 `````` (* application *) module HeapSort use import SkewHeaps use import int.Int use import ref.Ref use import array.Array use import array.ArrayPermut clone export array.Sorted with type elt = elt, predicate le = le use import map.Occ as M use import bintree.Occ as H let heapsort (a: array elt) : unit ensures { sorted a } ensures { permut_all (old a) a } = let n = length a in let t = ref (empty ()) in for i = 0 to n - 1 do invariant { heap !t && size !t = i } invariant { forall e. M.occ e a.elts i n + H.occ e !t = M.occ e a.elts 0 n } t := add a[i] !t; assert { M.occ a[i] a.elts i n = 1 + M.occ a[i] a.elts (i+1) n } done; 'I: for i = 0 to n - 1 do invariant { sorted_sub a 0 i } invariant { heap !t && size !t = n - i } invariant { forall j. 0 <= j < i -> forall e. mem e !t -> le a[j] e } invariant { forall e. M.occ e a.elts 0 i + H.occ e !t = M.occ e (at a.elts 'I) 0 n } a[i] <- get_min !t; t := remove_min !t done end``````