linear probing: work in progress

parent 7c52bade
......@@ -8,6 +8,7 @@ module LinearProbing
use import option.Option
use import list.Mem
use import map.Map
use import ref.Ref
use import array.Array
type key
......@@ -31,9 +32,17 @@ module LinearProbing
clone import array.NumOfEq with type elt = key
let rec lemma numof_eq (a1 a2: array key) (v: key) (l u: int) : unit
requires { 0 <= l <= u <= length a1 = length a2 }
requires { forall i: int. l <= i < u -> a2[i] = a1[i] }
ensures { numof a2 v l u = numof a1 v l u }
variant { u-l }
= if l < u then numof_eq a1 a2 v (l+1) u
type t = { mutable size: int; (* total number of elements *)
mutable data: array key; (* buckets *)
ghost mutable view: map key bool; (* pure model *)
ghost mutable loc : map key int; (* index where it is stored *)
}
(* at least one empty slot *)
invariant { 0 <= self.size < length self.data }
......@@ -47,9 +56,11 @@ module LinearProbing
(* any value in the model is in the array *)
invariant { let n = Array.length self.data in
forall x: key. Map.get self.view x ->
exists i: int. 0 <= i < n && self.data[i] = x &&
forall j: int. 0 <= j < n ->
between (bucket x n) j i -> self.data[j] <> dummy }
let i = Map.get self.loc x in
0 <= i < n && self.data[i] = x &&
forall j: int. 0 <= j < n ->
between (bucket x n) j i ->
self.data[j] <> x /\ self.data[j] <> dummy }
let rec lemma dummy_const (a: array key) (n: int)
requires { 0 <= n } requires { forall i: int. 0 <= i < n -> a[i] = dummy }
......@@ -60,7 +71,8 @@ module LinearProbing
requires { 0 < n }
ensures { forall x: key. not (Map.get result.view x) }
=
{ size = 0; data = Array.make n dummy; view = Map.const false; }
{ size = 0; data = Array.make n dummy;
view = Map.const false; loc = Map.const 0; }
let clear (h: t) : unit
writes { h.size, h.data.elts, h.view }
......@@ -84,6 +96,7 @@ module LinearProbing
a[j] <> x /\ a[j] <> dummy }
=
let n = Array.length a in
let ghost count = ref 0 in
let rec find (i: int) : int
requires { 0 <= i < n }
requires { forall j: int. 0 <= j < n -> between (bucket x n) j i ->
......@@ -104,53 +117,71 @@ module LinearProbing
h.data[find h.data x] <> dummy
let resize (h: t) : unit
writes { h.data }
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 (Map.const 0) in
for i = 0 to n - 1 do
invariant { numof a dummy 0 n2 = numof h.data dummy 0 i + n2 - i }
invariant { forall j: int. 0 <= j < n2 ->
a[i] <> dummy -> Map.get h.view a[i] }
invariant { forall j: int. 0 <= j < i -> let x = h.data[i] in
x <> dummy ->
exists j2: int. 0 <= j2 < n2 ->
a[j2] = x /\
a[j] <> dummy -> Map.get h.view a[j] }
invariant { forall x: key. Map.get h.view x ->
let j = Map.get h.loc x in
if j < i then
let j2 = Map.get !l x in
0 <= j2 < n2 /\ a[j2] = x /\
forall k: int. 0 <= k < n2 ->
between (bucket x n) k j2 -> a[k] <> dummy }
between (bucket x n2) k j2 -> a[k] <> x /\ a[k] <> dummy
else
forall j2: int. 0 <= j2 < n2 -> a[j2] <> x }
let x = h.data[i] in
if x <> dummy then a[find a x] <- x
if x <> dummy then begin
'L:
assert { Map.get h.loc x = i };
let j = find a x in
assert { a[j] = dummy };
a[j] <- x;
assert { numof a dummy 0 (j+1) = numof (at a 'L) dummy 0 (j+1) - 1 };
l := Map.set !l x j
end
done;
h.loc <- !l;
h.data <- a
let add (h: t) (x: key) : unit
requires { x <> dummy }
writes { h.size, h.data, h.data.elts, h.view }
writes { h.size, h.data, h.data.elts, h.view, h.loc }
ensures { h.view = Map.set (old h.view) x True }
=
if 2 * (h.size + 1) >= Array.length h.data then resize h;
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 h.data[i] = dummy then h.size <- h.size + 1;
if h.data[i] = dummy then begin
'L:
h.size <- h.size + 1;
h.data[i] <- x;
assert { numof h.data dummy 0 (i+1) =
numof (at h.data 'L) dummy 0 (i+1) - 1 }
end;
ghost h.view <- Map.set h.view x True;
h.data[i] <- x
ghost h.loc <- Map.set h.loc 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; }
end
(*
let resize h =
let old = h.data in
h.data <- Array.make (2 * Array.length h.data) h.dummy;
Array.iter (fun x -> h.data.(find h x) <- x) old
let add h x =
if 2 * h.size >= Array.length h.data then resize h;
let i = find h x in
if h.data.(i) == h.dummy then h.size <- h.size + 1;
h.data.(i) <- x
let remove h x =
let n = Array.length h.data in
let rec delete j i =
......@@ -172,19 +203,5 @@ end
h.size <- h.size - 1;
end
let iter f h =
Array.iter (fun x -> if x != h.dummy then f x) h.data
let fold f h init =
Array.fold_right (fun x acc -> if x != h.dummy then f x acc) h.data init
let copy h =
{ size = h.size; dummy = h.dummy; data = Array.copy h.data }
let print fmt h =
Format.fprintf fmt "size = %d, length = %d@." h.size (Array.length h.data);
Array.iter (fun x ->
Format.fprintf fmt "%c" (if x == h.dummy then '.' else '#')) h.data
*)
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment