skew_heaps.mlw 5.01 KB
 Jean-Christophe Filliatre committed May 17, 2014 1 `````` `````` 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 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 ``````module Heap use import int.Int type elt predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le type t function size t : int function occ elt t : int predicate mem (x: elt) (t: t) = occ x t > 0 function minimum t : elt predicate is_minimum (x: elt) (t: t) = mem x t && forall e. mem e t -> le x e axiom min_is_min: forall t: t. 0 < size t -> is_minimum (minimum t) t val empty () : t ensures { size result = 0 } ensures { forall e. not (mem e result) } val size (t: t) : int ensures { result = size t } val is_empty (t: t) : bool ensures { result <-> size t = 0 } val get_min (t: t) : elt requires { 0 < size t } ensures { result = minimum t } val merge (t1 t2: t) : t ensures { forall e. occ e result = occ e t1 + occ e t2 } ensures { size result = size t1 + size t2 } val add (x: elt) (t: t) : t ensures { occ x result = occ x t + 1 } ensures { forall e. e <> x -> occ e result = occ e t } ensures { size result = size t + 1 } val remove_min (t: t) : t requires { 0 < size t } 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 } end `````` Jean-Christophe Filliatre committed May 17, 2014 57 58 ``````module SkewHeaps `````` Guillaume Melquiond committed Aug 21, 2014 59 `````` use import int.Int `````` Jean-Christophe Filliatre committed May 17, 2014 60 `````` use import bintree.Tree `````` Jean-Christophe Filliatre committed May 17, 2014 61 62 `````` use export bintree.Size use export bintree.Occ `````` Jean-Christophe Filliatre committed May 17, 2014 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 `````` 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 81 82 83 `````` 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 84 85 86 87 `````` 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 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 `````` 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 113 `````` = `````` Jean-Christophe Filliatre committed May 17, 2014 114 `````` size t `````` Jean-Christophe Filliatre committed May 17, 2014 115 116 `````` let get_min (t: tree elt) : elt `````` Jean-Christophe Filliatre committed May 17, 2014 117 118 `````` requires { heap t && 0 < size t } ensures { result = minimum t } `````` Jean-Christophe Filliatre committed May 17, 2014 119 120 121 122 123 124 125 126 127 128 `````` = 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 129 `````` ensures { size result = size t1 + size t2 } `````` Jean-Christophe Filliatre committed May 17, 2014 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 `````` 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 146 147 `````` ensures { forall e. e <> x -> occ e result = occ e t } ensures { size result = size t + 1 } `````` Jean-Christophe Filliatre committed May 17, 2014 148 149 150 `````` = merge (Node Empty x Empty) t `````` Jean-Christophe Filliatre committed May 17, 2014 151 152 `````` let remove_min (t: tree elt) : tree elt requires { heap t && 0 < size t } `````` Jean-Christophe Filliatre committed May 17, 2014 153 `````` ensures { heap result } `````` Jean-Christophe Filliatre committed May 17, 2014 154 155 156 `````` 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 157 158 159 160 161 162 163 `````` = match t with | Empty -> absurd | Node l _ r -> merge l r end end `````` Jean-Christophe Filliatre committed May 17, 2014 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 `````` (* 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``````