linear_probing.mlw 11.2 KB
 Jean-Christophe Filliatre committed Apr 26, 2014 1 `````` `````` Jean-Christophe Filliatre committed Sep 01, 2014 2 3 ``````(** Hash tables using linear probing `````` Jean-Christophe Filliatre committed Sep 02, 2014 4 5 `````` Authors: Jean-Christophe Filliâtre (CNRS) Martin Clochard (École Normale Supérieure) `````` Jean-Christophe Filliatre committed Sep 01, 2014 6 ``````*) `````` Jean-Christophe Filliatre committed Apr 26, 2014 7 `````` `````` Jean-Christophe Filliatre committed Aug 27, 2014 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 ``````module HashedTypeWithDummy use import int.Int type key type keym (** the logic model of a key *) function keym key: keym predicate eq (x y: key) = keym x = keym y val eq (x y: key) : bool ensures { result <-> eq x y } predicate neq (x y: key) = keym x <> keym y let neq (x y: key) : bool ensures { result <-> neq x y } = not (eq x y) function hash key : int axiom hash_nonneg: forall k: key. 0 <= hash k axiom hash_eq: forall x y: key. eq x y -> hash x = hash y constant dummy: key constant dummym: keym = keym dummy end `````` Jean-Christophe Filliatre committed Apr 26, 2014 29 30 ``````module LinearProbing `````` Jean-Christophe Filliatre committed Aug 27, 2014 31 32 `````` clone import HashedTypeWithDummy `````` Jean-Christophe Filliatre committed Apr 26, 2014 33 34 35 36 37 `````` use import int.Int use import int.ComputerDivision use import option.Option use import list.Mem use import map.Map `````` MARCHE Claude committed Jul 06, 2015 38 `````` use map.Const `````` Jean-Christophe Filliatre committed Jun 20, 2014 39 `````` use import ref.Ref `````` Jean-Christophe Filliatre committed Apr 26, 2014 40 41 42 43 44 45 46 47 `````` use import array.Array function bucket (k: key) (n: int) : int = mod (hash k) n lemma bucket_bounds: forall n: int. 0 < n -> forall k: key. 0 <= bucket k n < n `````` Jean-Christophe Filliatre committed Aug 27, 2014 48 `````` (** j lies between l and r, cyclically *) `````` Jean-Christophe Filliatre committed Apr 26, 2014 49 `````` predicate between (l j r: int) = `````` Jean-Christophe Filliatre committed Jun 16, 2014 50 `````` l <= j < r || r < l <= j || j < r < l `````` Jean-Christophe Filliatre committed Apr 26, 2014 51 `````` `````` Jean-Christophe Filliatre committed Aug 27, 2014 52 53 `````` (** number of dummy values in array [a] between [l] and [u] *) namespace NumOfDummy `````` Jean-Christophe Filliatre committed Nov 23, 2014 54 55 56 57 `````` use int.NumOf function numof (a: array key) (l u: int) : int = NumOf.numof (\ i. eq a[i] dummy) l u `````` Jean-Christophe Filliatre committed Apr 26, 2014 58 `````` `````` Jean-Christophe Filliatre committed Aug 27, 2014 59 60 61 `````` let rec lemma numof_eq (a1 a2: array key) (l u: int) : unit requires { 0 <= l <= u <= length a1 = length a2 } requires { forall i: int. l <= i < u -> eq a2[i] a1[i] } `````` Jean-Christophe Filliatre committed Nov 23, 2014 62 `````` ensures { numof a2 l u = numof a1 l u } `````` Jean-Christophe Filliatre committed Aug 27, 2014 63 64 65 66 67 `````` variant { u-l } = if l < u then numof_eq a1 a2 (l+1) u let rec lemma dummy_const (a: array key) (n: int) requires { 0 <= n } requires { forall i: int. 0 <= i < n -> a[i] = dummy } `````` Jean-Christophe Filliatre committed Nov 23, 2014 68 `````` variant { n } ensures { numof a 0 n = n } `````` Jean-Christophe Filliatre committed Aug 27, 2014 69 `````` = if n > 0 then dummy_const a (n-1) `````` Jean-Christophe Filliatre committed Sep 01, 2014 70 `````` `````` Jean-Christophe Filliatre committed Aug 27, 2014 71 `````` end `````` Jean-Christophe Filliatre committed Nov 23, 2014 72 `````` function numofd (a: array key) (l u: int) : int = NumOfDummy.numof a l u `````` Jean-Christophe Filliatre committed Jun 20, 2014 73 `````` `````` Jean-Christophe Filliatre committed Sep 01, 2014 74 75 76 77 78 79 80 81 82 83 84 85 86 `````` let ghost numof_update (a1 a2: array key) (l i u: int) requires { 0 <= l <= i < u <= Array.length a1 = Array.length a2 } requires { forall j: int. l <= j < u -> j<>i -> a1[j] = a2[j] } requires { eq a1[i] dummy && neq a2[i] dummy } ensures { numofd a1 l u = 1 + numofd a2 l u } = assert { numofd a1 l u = numofd a1 l i + numofd a1 i u = numofd a1 l i + numofd a1 i (i+1) + numofd a1 (i+1) u }; assert { numofd a2 l u = numofd a2 l i + numofd a2 i u = numofd a2 l i + numofd a2 i (i+1) + numofd a2 (i+1) u } `````` Jean-Christophe Filliatre committed Sep 01, 2014 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 `````` predicate valid (data: array key) (view: map keym bool) (loc : map keym int) = (* dummy not in the model *) not (Map.get view dummym) /\ (* any value in the array is in the model *) (forall i: int. 0 <= i < Array.length data -> let x = data[i] in neq x dummy -> Map.get view (keym x) /\ Map.get loc (keym x) = i) /\ (* any value in the model is in the array *) (let n = Array.length data in forall x: key. Map.get view (keym x) -> let i = Map.get loc (keym x) in 0 <= i < n && eq data[i] x && forall j: int. 0 <= j < n -> between (bucket x n) j i -> neq data[j] x /\ neq data[j] dummy) (* TODO ^^^^^^^^^^^^^^^^^^ is actually provable *) `````` Jean-Christophe Filliatre committed Apr 26, 2014 106 107 `````` type t = { mutable size: int; (* total number of elements *) mutable data: array key; (* buckets *) `````` Jean-Christophe Filliatre committed Aug 27, 2014 108 109 `````` ghost mutable view: map keym bool; (* pure model *) ghost mutable loc : map keym int; (* index where it is stored *) `````` Jean-Christophe Filliatre committed Apr 26, 2014 110 111 112 113 `````` } (* at least one empty slot *) invariant { 0 <= self.size < length self.data } invariant { let n = Array.length self.data in `````` Jean-Christophe Filliatre committed Aug 27, 2014 114 `````` self.size + numofd self.data 0 n = n } `````` Jean-Christophe Filliatre committed Sep 01, 2014 115 `````` invariant { valid self.data self.view self.loc } `````` Jean-Christophe Filliatre committed Apr 26, 2014 116 117 118 `````` let create (n: int) : t requires { 0 < n } `````` Jean-Christophe Filliatre committed Aug 27, 2014 119 `````` ensures { forall x: key. not (Map.get result.view (keym x)) } `````` Jean-Christophe Filliatre committed Apr 26, 2014 120 `````` = `````` Jean-Christophe Filliatre committed Jun 20, 2014 121 `````` { size = 0; data = Array.make n dummy; `````` MARCHE Claude committed Jul 06, 2015 122 `````` view = Const.const false; loc = Const.const 0; } `````` Jean-Christophe Filliatre committed Apr 26, 2014 123 124 125 126 `````` let clear (h: t) : unit writes { h.size, h.data.elts, h.view } ensures { h.size = 0 } `````` Jean-Christophe Filliatre committed Aug 27, 2014 127 `````` ensures { forall x: key. not (Map.get h.view (keym x)) } `````` Jean-Christophe Filliatre committed Apr 26, 2014 128 129 130 `````` = h.size <- 0; Array.fill h.data 0 (Array.length h.data) dummy; `````` MARCHE Claude committed Jul 06, 2015 131 `````` h.view <- Const.const false `````` Jean-Christophe Filliatre committed Apr 26, 2014 132 133 134 135 `````` function next (n i: int) : int = let i = i+1 in if i = n then 0 else i `````` Jean-Christophe Filliatre committed Jun 16, 2014 136 `````` let find (a: array key) (x: key) : int `````` Jean-Christophe Filliatre committed Aug 27, 2014 137 138 `````` requires { neq x dummy } requires { let n = Array.length a in 0 < n /\ numofd a 0 n > 0 } `````` Jean-Christophe Filliatre committed Jun 16, 2014 139 `````` ensures { 0 <= result < Array.length a } `````` Jean-Christophe Filliatre committed Aug 27, 2014 140 `````` ensures { eq a[result] dummy || eq a[result] x } `````` Jean-Christophe Filliatre committed Jun 16, 2014 141 142 `````` ensures { forall j: int. 0 <= j < Array.length a -> between (bucket x (Array.length a)) j result -> `````` Jean-Christophe Filliatre committed Aug 27, 2014 143 `````` neq a[j] x /\ neq a[j] dummy } `````` Jean-Christophe Filliatre committed Apr 26, 2014 144 `````` = `````` Jean-Christophe Filliatre committed Jun 16, 2014 145 `````` let n = Array.length a in `````` Jean-Christophe Filliatre committed Jun 27, 2014 146 `````` let b = bucket x n in `````` Jean-Christophe Filliatre committed Apr 26, 2014 147 148 `````` let rec find (i: int) : int requires { 0 <= i < n } `````` Jean-Christophe Filliatre committed Aug 27, 2014 149 `````` requires { numofd a 0 n > 0 } `````` Jean-Christophe Filliatre committed Jun 27, 2014 150 `````` requires { forall j: int. 0 <= j < n -> between b j i -> `````` Jean-Christophe Filliatre committed Aug 27, 2014 151 152 153 `````` neq a[j] x /\ neq a[j] dummy } requires { if i >= b then numofd a b i = 0 else numofd a b n = numofd a 0 i = 0 } `````` Jean-Christophe Filliatre committed Jun 27, 2014 154 `````` variant { if i >= b then n - i + b else b - i } `````` Jean-Christophe Filliatre committed Apr 26, 2014 155 `````` ensures { 0 <= result < n } `````` Jean-Christophe Filliatre committed Aug 27, 2014 156 `````` ensures { eq a[result] dummy || eq a[result] x } `````` Jean-Christophe Filliatre committed Jun 27, 2014 157 `````` ensures { forall j: int. 0 <= j < n -> between b j result -> `````` Jean-Christophe Filliatre committed Aug 27, 2014 158 `````` neq a[j] x /\ neq a[j] dummy } `````` Jean-Christophe Filliatre committed Apr 26, 2014 159 `````` = `````` Jean-Christophe Filliatre committed Aug 27, 2014 160 `````` if eq a[i] dummy || eq a[i] x then i else find (next n i) `````` Jean-Christophe Filliatre committed Apr 26, 2014 161 `````` in `````` Jean-Christophe Filliatre committed Jun 27, 2014 162 `````` find b `````` Jean-Christophe Filliatre committed Apr 26, 2014 163 `````` `````` Jean-Christophe Filliatre committed Jun 16, 2014 164 `````` let mem (h: t) (x: key) : bool `````` Jean-Christophe Filliatre committed Aug 27, 2014 165 166 `````` requires { neq x dummy } ensures { result <-> Map.get h.view (keym x) } `````` Jean-Christophe Filliatre committed Jun 16, 2014 167 `````` = `````` Jean-Christophe Filliatre committed Aug 27, 2014 168 `````` neq h.data[find h.data x] dummy `````` Jean-Christophe Filliatre committed Jun 16, 2014 169 170 `````` let resize (h: t) : unit `````` Jean-Christophe Filliatre committed Jun 20, 2014 171 `````` writes { h.data, h.loc } `````` Jean-Christophe Filliatre committed Jun 16, 2014 172 173 174 175 176 `````` ensures { Array.length h.data = 2 * old (Array.length h.data) } = let n = Array.length h.data in let n2 = 2 * n in let a = Array.make n2 dummy in `````` MARCHE Claude committed Jul 06, 2015 177 `````` let ghost l = ref (Const.const 0) in `````` Jean-Christophe Filliatre committed Jun 16, 2014 178 `````` for i = 0 to n - 1 do `````` Jean-Christophe Filliatre committed Aug 27, 2014 179 180 181 182 183 `````` invariant { numofd a 0 n2 = numofd h.data 0 i + n2 - i } invariant { forall j: int. 0 <= j < n2 -> neq a[j] dummy -> Map.get h.view (keym a[j]) /\ Map.get !l (keym a[j]) = j } invariant { forall x: key. Map.get h.view (keym x) -> let j = Map.get h.loc (keym x) in `````` Jean-Christophe Filliatre committed Jun 20, 2014 184 `````` if j < i then `````` Jean-Christophe Filliatre committed Aug 27, 2014 185 186 `````` let j2 = Map.get !l (keym x) in 0 <= j2 < n2 /\ eq a[j2] x /\ `````` Jean-Christophe Filliatre committed Jun 16, 2014 187 `````` forall k: int. 0 <= k < n2 -> `````` Jean-Christophe Filliatre committed Aug 27, 2014 188 `````` between (bucket x n2) k j2 -> neq a[k] x /\ neq a[k] dummy `````` Jean-Christophe Filliatre committed Jun 20, 2014 189 `````` else `````` Jean-Christophe Filliatre committed Aug 27, 2014 190 `````` forall j2: int. 0 <= j2 < n2 -> neq a[j2] x } `````` Jean-Christophe Filliatre committed Jun 16, 2014 191 `````` let x = h.data[i] in `````` Jean-Christophe Filliatre committed Aug 27, 2014 192 `````` if neq x dummy then begin `````` Jean-Christophe Filliatre committed Jun 20, 2014 193 194 `````` 'L: let j = find a x in `````` Jean-Christophe Filliatre committed Aug 27, 2014 195 `````` assert { eq a[j] dummy }; `````` Jean-Christophe Filliatre committed Jun 20, 2014 196 `````` a[j] <- x; `````` Jean-Christophe Filliatre committed Aug 27, 2014 197 198 `````` assert { numofd a 0 (j+1) = numofd (at a 'L) 0 (j+1) - 1 }; l := Map.set !l (keym x) j `````` Jean-Christophe Filliatre committed Jun 20, 2014 199 `````` end `````` Jean-Christophe Filliatre committed Jun 16, 2014 200 `````` done; `````` Jean-Christophe Filliatre committed Jun 20, 2014 201 `````` h.loc <- !l; `````` Jean-Christophe Filliatre committed Jun 16, 2014 202 203 204 `````` h.data <- a let add (h: t) (x: key) : unit `````` Jean-Christophe Filliatre committed Aug 27, 2014 205 `````` requires { neq x dummy } `````` Jean-Christophe Filliatre committed Jun 20, 2014 206 `````` writes { h.size, h.data, h.data.elts, h.view, h.loc } `````` Jean-Christophe Filliatre committed Aug 27, 2014 207 `````` ensures { h.view = Map.set (old h.view) (keym x) True } `````` Jean-Christophe Filliatre committed Jun 16, 2014 208 `````` = `````` Jean-Christophe Filliatre committed Jun 20, 2014 209 210 211 212 `````` abstract ensures { h.size + 1 < Array.length h.data } if 2 * (h.size + 1) >= Array.length h.data then resize h end; `````` Jean-Christophe Filliatre committed Jun 16, 2014 213 `````` let i = find h.data x in `````` Jean-Christophe Filliatre committed Aug 27, 2014 214 `````` if eq h.data[i] dummy then begin `````` Jean-Christophe Filliatre committed Jun 20, 2014 215 216 217 `````` 'L: h.size <- h.size + 1; h.data[i] <- x; `````` Jean-Christophe Filliatre committed Aug 27, 2014 218 219 `````` assert { numofd h.data 0 (i+1) = numofd (at h.data 'L) 0 (i+1) - 1 } `````` Jean-Christophe Filliatre committed Jun 20, 2014 220 `````` end; `````` Jean-Christophe Filliatre committed Aug 27, 2014 221 222 `````` ghost h.view <- Map.set h.view (keym x) True; ghost h.loc <- Map.set h.loc (keym x) i; `````` Jean-Christophe Filliatre committed Jun 20, 2014 223 224 225 226 227 228 229 `````` () let copy (h: t) : t ensures { result.view = h.view } = { size = h.size; data = Array.copy h.data; view = h.view; loc = h.loc; } `````` Jean-Christophe Filliatre committed Jun 16, 2014 230 `````` `````` Jean-Christophe Filliatre committed Sep 01, 2014 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 `````` let rec ghost find_dummy (a: array key) (s: int) (i: int) : int requires { 0 <= s < Array.length a } requires { 0 <= i < Array.length a } requires { i <> s } requires { if i >= s then numofd a i (Array.length a) + numofd a 0 s >= 1 else numofd a i s >= 1} requires { forall k: int. 0 <= k < Array.length a -> between s k i -> k<>s -> neq a[k] dummy } variant { if i >= s then Array.length a - i + s else s - i} ensures { 0 <= result < Array.length a } ensures { result <> s } ensures { eq a[result] dummy } ensures { forall k: int. 0 <= k < Array.length a -> between s k result -> k<>s -> neq a[k] dummy } = let n = Array.length a in if eq a[i] dummy then i else find_dummy a s (next n i) `````` Jean-Christophe Filliatre committed Sep 01, 2014 249 250 251 252 253 `````` (* j is the hole just created by remove (see below) and this function restores the data structure invariant for elements to the right of j if needed, starting at index i *) let rec delete (a: array key) (ghost loc: ref (map keym int)) (ghost view: map keym bool) `````` Jean-Christophe Filliatre committed Sep 01, 2014 254 255 `````` (ghost f0: int) (j i: int) : unit requires { 0 <= f0 < Array.length a } `````` Jean-Christophe Filliatre committed Aug 27, 2014 256 257 `````` requires { 0 <= j < Array.length a } requires { 0 <= i < Array.length a } `````` Jean-Christophe Filliatre committed Sep 01, 2014 258 259 260 261 262 263 `````` requires { j <> f0 } requires { eq a[j] dummy } requires { eq a[f0] dummy } requires { between j i f0 } requires { forall k: int. 0 <= k < Array.length a -> between i k f0 -> k<>i -> neq a[k] dummy } `````` Jean-Christophe Filliatre committed Sep 01, 2014 264 `````` requires { not (Map.get view dummym) } `````` Jean-Christophe Filliatre committed Aug 27, 2014 265 `````` requires { forall k: int. 0 <= k < Array.length a -> `````` Jean-Christophe Filliatre committed Sep 01, 2014 266 267 268 269 270 271 272 273 274 275 276 `````` let x = a[k] in neq x dummy -> Map.get view (keym x) /\ Map.get !loc (keym x) = k } (* any value in the model is in the array *) requires { let n = Array.length a in forall x: key. Map.get view (keym x) -> let k = Map.get !loc (keym x) in 0 <= k < n && eq a[k] x && forall l: int. 0 <= l < n -> between (bucket x n) l k -> neq a[l] x /\ (neq a[l] dummy \/ l = j /\ between j i k) } `````` Jean-Christophe Filliatre committed Sep 01, 2014 277 `````` variant { if i >= f0 then Array.length a - i + f0 else f0 - i } `````` Jean-Christophe Filliatre committed Aug 27, 2014 278 279 `````` ensures { numofd a 0 (Array.length a) = numofd (old a) 0 (Array.length a) } `````` Jean-Christophe Filliatre committed Sep 01, 2014 280 `````` ensures { valid a view !loc } `````` Jean-Christophe Filliatre committed Aug 27, 2014 281 282 283 284 285 286 287 `````` = let n = Array.length a in let i = next n i in let xi = a[i] in if neq xi dummy then begin let r = bucket xi n in if j < r && r <= i || i < j && j < r || r <= i && i < j then `````` Jean-Christophe Filliatre committed Sep 01, 2014 288 `````` (* the hash index r lies cyclically between j and i *) `````` Jean-Christophe Filliatre committed Sep 01, 2014 289 `````` delete a loc view f0 j i `````` Jean-Christophe Filliatre committed Aug 27, 2014 290 `````` else begin `````` Jean-Christophe Filliatre committed Sep 01, 2014 291 292 `````` let ghost a1 = Array.copy a in ghost NumOfDummy.numof_eq a a1 0 n; `````` Jean-Christophe Filliatre committed Sep 01, 2014 293 `````` (* the hole j lies cyclically between hash index r and i *) `````` Jean-Christophe Filliatre committed Sep 01, 2014 294 295 296 297 298 `````` a[j] <- xi; ghost numof_update a1 a 0 j n; let ghost a2 = Array.copy a in ghost NumOfDummy.numof_eq a a2 0 n; ghost loc := Map.set !loc (keym xi) j; `````` Jean-Christophe Filliatre committed Aug 27, 2014 299 `````` a[i] <- dummy; `````` Jean-Christophe Filliatre committed Sep 01, 2014 300 301 `````` ghost numof_update a a2 0 i n; delete a loc view f0 i i `````` Jean-Christophe Filliatre committed Aug 27, 2014 302 303 304 `````` end end `````` Jean-Christophe Filliatre committed Jun 21, 2014 305 `````` let remove (h: t) (x: key) : unit `````` Jean-Christophe Filliatre committed Aug 27, 2014 306 307 `````` requires { neq x dummy } ensures { h.view = Map.set (old h.view) (keym x) False } `````` Jean-Christophe Filliatre committed Jun 27, 2014 308 `````` = `````` Jean-Christophe Filliatre committed Sep 01, 2014 309 `````` let n = Array.length h.data in `````` Jean-Christophe Filliatre committed Jun 21, 2014 310 `````` let j = find h.data x in `````` Jean-Christophe Filliatre committed Aug 27, 2014 311 `````` if neq h.data[j] dummy then begin `````` Jean-Christophe Filliatre committed Jun 21, 2014 312 313 `````` 'L: h.data[j] <- dummy; `````` Jean-Christophe Filliatre committed Sep 01, 2014 314 `````` assert { numofd h.data 0 (j+1) = `````` Jean-Christophe Filliatre committed Aug 27, 2014 315 316 `````` numofd (at h.data 'L) 0 (j+1) + 1 }; ghost h.view <- Map.set h.view (keym x) False; `````` Jean-Christophe Filliatre committed Jun 27, 2014 317 `````` let l = ref h.loc in `````` Jean-Christophe Filliatre committed Sep 01, 2014 318 319 `````` let f0 = find_dummy h.data j (next n j) in delete h.data l h.view f0 j j; `````` Jean-Christophe Filliatre committed Jun 27, 2014 320 `````` ghost h.loc <- !l; `````` Jean-Christophe Filliatre committed Apr 26, 2014 321 322 323 `````` h.size <- h.size - 1; end `````` Jean-Christophe Filliatre committed Jun 21, 2014 324 ``end``