skew_heaps.mlw 5.07 KB
 Jean-Christophe Filliatre committed May 17, 2014 1 `````` `````` Jean-Christophe Filliatre committed Sep 02, 2014 2 3 4 5 6 ``````(** Skew heaps Author: Jean-Christophe Filliâtre (CNRS) *) `````` 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 57 58 59 60 61 ``````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 62 63 ``````module SkewHeaps `````` Guillaume Melquiond committed Aug 21, 2014 64 `````` use import int.Int `````` Jean-Christophe Filliatre committed May 17, 2014 65 `````` use import bintree.Tree `````` Jean-Christophe Filliatre committed May 17, 2014 66 67 `````` use export bintree.Size use export bintree.Occ `````` Jean-Christophe Filliatre committed May 17, 2014 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 `````` 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 86 87 88 `````` 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 89 90 91 92 `````` 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 93 94 95 `````` let rec lemma root_is_min (t: tree elt) : unit requires { heap t && 0 < size t } ensures { is_minimum (minimum t) t } `````` Jean-Christophe Filliatre committed Oct 26, 2014 96 `````` variant { t } `````` Jean-Christophe Filliatre committed May 17, 2014 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 `````` = 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 118 `````` = `````` Jean-Christophe Filliatre committed May 17, 2014 119 `````` size t `````` Jean-Christophe Filliatre committed May 17, 2014 120 121 `````` let get_min (t: tree elt) : elt `````` Jean-Christophe Filliatre committed May 17, 2014 122 123 `````` requires { heap t && 0 < size t } ensures { result = minimum t } `````` Jean-Christophe Filliatre committed May 17, 2014 124 125 126 127 128 129 130 131 132 133 `````` = 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 134 `````` ensures { size result = size t1 + size t2 } `````` Jean-Christophe Filliatre committed May 17, 2014 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 `````` 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 151 152 `````` ensures { forall e. e <> x -> occ e result = occ e t } ensures { size result = size t + 1 } `````` Jean-Christophe Filliatre committed May 17, 2014 153 154 155 `````` = merge (Node Empty x Empty) t `````` Jean-Christophe Filliatre committed May 17, 2014 156 157 `````` let remove_min (t: tree elt) : tree elt requires { heap t && 0 < size t } `````` Jean-Christophe Filliatre committed May 17, 2014 158 `````` ensures { heap result } `````` Jean-Christophe Filliatre committed May 17, 2014 159 160 161 `````` 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 162 163 164 165 166 167 168 `````` = match t with | Empty -> absurd | Node l _ r -> merge l r end end `````` Jean-Christophe Filliatre committed May 17, 2014 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 203 204 205 206 207 `````` (* 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``````