(** Hash tables using linear probing Authors: Jean-Christophe Filliâtre (CNRS) Martin Clochard (École Normale Supérieure) *) 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 module LinearProbing clone import HashedTypeWithDummy use import int.Int use import int.ComputerDivision use import option.Option use import list.Mem use import map.Map use map.Const use import ref.Ref 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 (** j lies between l and r, cyclically *) predicate between (l j r: int) = l <= j < r || r < l <= j || j < r < l (** number of dummy values in array [a] between [l] and [u] *) namespace NumOfDummy use int.NumOf function numof (a: array key) (l u: int) : int = NumOf.numof (\ i. eq a[i] dummy) l u 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] } ensures { numof a2 l u = numof a1 l u } 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 } variant { n } ensures { numof a 0 n = n } = if n > 0 then dummy_const a (n-1) end function numofd (a: array key) (l u: int) : int = NumOfDummy.numof a l u 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 } 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 *) type t = { mutable size: int; (* total number of elements *) mutable data: array key; (* buckets *) ghost mutable view: map keym bool; (* pure model *) ghost mutable loc : map keym int; (* index where it is stored *) } (* at least one empty slot *) invariant { 0 <= self.size < length self.data } invariant { let n = Array.length self.data in self.size + numofd self.data 0 n = n } invariant { valid self.data self.view self.loc } let create (n: int) : t requires { 0 < n } ensures { forall x: key. not (Map.get result.view (keym x)) } = { size = 0; data = Array.make n dummy; view = Const.const false; loc = Const.const 0; } let clear (h: t) : unit writes { h.size, h.data.elts, h.view } ensures { h.size = 0 } ensures { forall x: key. not (Map.get h.view (keym x)) } = h.size <- 0; Array.fill h.data 0 (Array.length h.data) dummy; h.view <- Const.const false function next (n i: int) : int = let i = i+1 in if i = n then 0 else i let find (a: array key) (x: key) : int requires { neq x dummy } requires { let n = Array.length a in 0 < n /\ numofd a 0 n > 0 } ensures { 0 <= result < Array.length a } ensures { eq a[result] dummy || eq a[result] x } ensures { forall j: int. 0 <= j < Array.length a -> between (bucket x (Array.length a)) j result -> neq a[j] x /\ neq a[j] dummy } = let n = Array.length a in let b = bucket x n in let rec find (i: int) : int requires { 0 <= i < n } requires { numofd a 0 n > 0 } requires { forall j: int. 0 <= j < n -> between b j i -> 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 } variant { if i >= b then n - i + b else b - i } ensures { 0 <= result < n } ensures { eq a[result] dummy || eq a[result] x } ensures { forall j: int. 0 <= j < n -> between b j result -> neq a[j] x /\ neq a[j] dummy } = if eq a[i] dummy || eq a[i] x then i else find (next n i) in find b let mem (h: t) (x: key) : bool requires { neq x dummy } ensures { result <-> Map.get h.view (keym x) } = neq h.data[find h.data x] dummy let resize (h: t) : unit writes { h.data, h.loc } 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 let ghost l = ref (Const.const 0) in for i = 0 to n - 1 do 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 if j < i then let j2 = Map.get !l (keym x) in 0 <= j2 < n2 /\ eq a[j2] x /\ forall k: int. 0 <= k < n2 -> between (bucket x n2) k j2 -> neq a[k] x /\ neq a[k] dummy else forall j2: int. 0 <= j2 < n2 -> neq a[j2] x } let x = h.data[i] in if neq x dummy then begin 'L: let j = find a x in assert { eq a[j] dummy }; a[j] <- x; assert { numofd a 0 (j+1) = numofd (at a 'L) 0 (j+1) - 1 }; l := Map.set !l (keym x) j end done; h.loc <- !l; h.data <- a let add (h: t) (x: key) : unit requires { neq x dummy } writes { h.size, h.data, h.data.elts, h.view, h.loc } ensures { h.view = Map.set (old h.view) (keym x) True } = abstract ensures { h.size + 1 < Array.length h.data } if 2 * (h.size + 1) >= Array.length h.data then resize h end; let i = find h.data x in if eq h.data[i] dummy then begin 'L: h.size <- h.size + 1; h.data[i] <- x; assert { numofd h.data 0 (i+1) = numofd (at h.data 'L) 0 (i+1) - 1 } end; ghost h.view <- Map.set h.view (keym x) True; ghost h.loc <- Map.set h.loc (keym x) i; () let copy (h: t) : t ensures { result.view = h.view } = { size = h.size; data = Array.copy h.data; view = h.view; loc = h.loc; } 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) (* 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) (ghost f0: int) (j i: int) : unit requires { 0 <= f0 < Array.length a } requires { 0 <= j < Array.length a } requires { 0 <= i < Array.length a } 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 } requires { not (Map.get view dummym) } requires { forall k: int. 0 <= k < Array.length a -> 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) } variant { if i >= f0 then Array.length a - i + f0 else f0 - i } ensures { numofd a 0 (Array.length a) = numofd (old a) 0 (Array.length a) } ensures { valid a view !loc } = 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 (* the hash index r lies cyclically between j and i *) delete a loc view f0 j i else begin let ghost a1 = Array.copy a in ghost NumOfDummy.numof_eq a a1 0 n; (* the hole j lies cyclically between hash index r and i *) 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; a[i] <- dummy; ghost numof_update a a2 0 i n; delete a loc view f0 i i end end let remove (h: t) (x: key) : unit requires { neq x dummy } ensures { h.view = Map.set (old h.view) (keym x) False } = let n = Array.length h.data in let j = find h.data x in if neq h.data[j] dummy then begin 'L: h.data[j] <- dummy; assert { numofd h.data 0 (j+1) = numofd (at h.data 'L) 0 (j+1) + 1 }; ghost h.view <- Map.set h.view (keym x) False; let l = ref h.loc in let f0 = find_dummy h.data j (next n j) in delete h.data l h.view f0 j j; ghost h.loc <- !l; h.size <- h.size - 1; end end