examples/linear_probing.mlw

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