remove_duplicate.mlw 2.02 KB
Newer Older
1

2 3 4

(** {1 Removing duplicate elements in an array}

5 6 7
    Given an array `a` of size `n`, removes its duplicate elements,
    in-place, as follows: return `r` such that `a[0..r-1]` contains the same
    elements as `a[0..n-1]` and no duplicate
8 9 10 11 12

*)


(** {2 Specification} *)
13 14 15 16 17 18

module Spec

  use export int.Int
  use export array.Array

19
  (** `v` appears in `a[0..s-1]` *)
20 21 22
  predicate appears (v: 'a) (a: array 'a) (s: int) =
    exists i: int. 0 <= i < s /\ a[i] = v

23
  (** `a[0..s-1]` contains no duplicate element *)
24 25 26 27 28
  predicate nodup (a: array 'a) (s: int) =
    forall i: int. 0 <= i < s -> not (appears a[i] a i)

end

29
(** {2 Quadratic implementation, without extra space} *)
30 31 32

module RemoveDuplicateQuadratic

33 34
  use Spec
  use ref.Refint
35

36 37 38 39 40
  type t
  val predicate eq (x y: t)
    ensures { result <-> x = y }

  let rec test_appears (ghost w: ref int) (v: t) (a: array t) (s: int) : bool
41
    requires { 0 <= s <= length a }
42 43
    ensures  { result <-> appears v a s }
    ensures  { result -> 0 <= !w < s && a[!w] = v }
44
    variant  { s }
45
  = s > 0 &&
46
    if eq a[s-1] v then begin w := s - 1; true end else test_appears w v a (s-1)
47

48
  let remove_duplicate (a: array t): int
49 50
    ensures { 0 <= result <= length a }
    ensures { nodup a result }
51
    ensures { forall v. appears v (old a) (length a) <-> appears v a result }
52 53
  = let n = length a in
    let r = ref 0 in
54
    let ghost from = make n 0 in
55
    let ghost to_  = make n 0 in
56 57 58
    for i = 0 to n - 1 do
      invariant { 0 <= !r <= i }
      invariant { nodup a !r }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
59
      invariant { forall j: int. 0 <= j < !r ->
60
                  0 <= to_[j] < i /\ a[j] = (old a)[to_[j]] }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
61
      invariant { forall j: int. 0 <= j < i ->
62 63
                  0 <= from[j] < !r /\ (old a)[j] = a[from[j]] }
      invariant { forall j: int. i <= j < n -> a[j] = (old a)[j] }
64 65 66 67 68 69 70 71 72 73
      let ghost w = ref 0 in
      if not (test_appears w a[i] a !r) then begin
        a[!r] <- a[i];
        from[i] <- !r;
        to_[!r] <- i;
        incr r
      end else begin
        from[i] <- !w;
        ()
      end
74 75 76 77
    done;
    !r

end