examples/remove_duplicate_hash.mlw

   1
   2
   3 (** {1 Removing duplicate elements in an array, using a mutable set}
   4
   5     Given an array `a` of size `n`, returns a fresh array containing
   6     the elements of `a` without duplicates, using a mutable set
   7     (typically a hash table).
   8
   9 *)
  10
  11 (** {2 Specification} *)
  12
  13 module Spec
  14
  15   use export int.Int
  16   use export array.Array
  17
  18   (** `v` appears in `a[0..s-1]` *)
  19   predicate appears (v: 'a) (a: array 'a) (s: int) =
  20     exists i: int. 0 <= i < s /\ a[i] = v
  21
  22   (** `a[0..s-1]` contains no duplicate element *)
  23   predicate nodup (a: array 'a) (s: int) =
  24     forall i: int. 0 <= i < s -> not (appears a[i] a i)
  25
  26 end
  27
  28 (** {2 Quadratic implementation, without extra space} *)
  29
  30 module RemoveDuplicate
  31
  32   use Spec
  33   use ref.Refint
  34   use array.Array
  35
  36   type elt
  37   clone import set.SetImp as MutableSet with type elt = elt
  38
  39   let remove_duplicate (a: array elt) : array elt
  40     requires { 1 <= length a }
  41     ensures  { nodup result (length result) }
  42     ensures  { forall x: elt.
  43                appears x a (length a) <-> appears x result (length result) }
  44   =
  45     let s = MutableSet.empty () in
  46     for i = 0 to Array.length a - 1 do
  47       invariant { forall x: elt. appears x a i <-> mem x s }
  48       MutableSet.add a[i] s
  49     done;
  50     label L in
  51     let r = Array.make (MutableSet.cardinal s) a[0] in
  52     MutableSet.clear s;
  53     let j = ref 0 in
  54     for i = 0 to Array.length a - 1 do
  55       invariant { forall x: elt. appears x a i <-> mem x s }
  56       invariant { forall x: elt. mem x s <-> appears x r !j }
  57       invariant { nodup r !j }
  58       invariant { 0 <= !j = cardinal s <= length r }
  59       invariant { subset s (s at L) }
  60       if not (MutableSet.mem a[i] s) then begin
  61         MutableSet.add a[i] s;
  62         r[!j] <- a[i];
  63         incr j
  64       end
  65     done;
  66     r
  67
  68 end