Wiki Agenda Contact Version française

Removing duplicate elements in an array, using a mutable set


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


Removing duplicate elements in an array, using a mutable set

Given an array a of size n, returns a fresh array containing the elements of a without duplicates, using a mutable set (typically a hash table).

Specification

module Spec

  use export int.Int
  use export array.Array

  predicate appears (v: 'a) (a: array 'a) (s: int) =
    exists i: int. 0 <= i < s /\ a[i] = v

v appears in a[0..s-1]

  predicate nodup (a: array 'a) (s: int) =
    forall i: int. 0 <= i < s -> not (appears a[i] a i)

a[0..s-1] contains no duplicate element

end

module MutableSet

  use set.Fset

  type elt

  type t = private { ghost mutable s: set elt }

  val create () : t
    ensures { is_empty result.s }

  val add (t: t) (x: elt) : unit
    writes  { t.s }
    ensures { t.s = add x (old t.s) }

  val contains (t: t) (x: elt) : bool
    ensures { result <-> mem x t.s }

  val clear (t: t) : unit
    writes  { t.s }
    ensures { is_empty t.s }

  val size (t: t) : int
    ensures { result = cardinal t.s }

end

Quadratic implementation, without extra space

module RemoveDuplicate

  use Spec
  use set.Fset
  use MutableSet
  use ref.Refint
  use array.Array

  let remove_duplicate (a: array elt) : array elt
    requires { 1 <= length a }
    ensures  { nodup result (length result) }
    ensures  { forall x: elt.
               appears x a (length a) <-> appears x result (length result) }
  =
    let s = MutableSet.create () in
    for i = 0 to Array.length a - 1 do
      invariant { forall x: elt. appears x a i <-> mem x s.s }
      MutableSet.add s a[i]
    done;
    label L in
    let r = Array.make (MutableSet.size s) a[0] in
    MutableSet.clear s;
    let j = ref 0 in
    for i = 0 to Array.length a - 1 do
      invariant { forall x: elt. appears x a i <-> mem x s.s }
      invariant { forall x: elt. mem x s.s <-> appears x r !j }
      invariant { nodup r !j }
      invariant { 0 <= !j = cardinal s.s <= length r }
      invariant { subset s.s (s.s at L) }
      if not (MutableSet.contains s a[i]) then begin
        MutableSet.add s a[i];
        r[!j] <- a[i];
        incr j
      end
    done;
    r

end

download ZIP archive

Why3 Proof Results for Project "remove_duplicate_hash"

Theory "remove_duplicate_hash.RemoveDuplicate": fully verified

ObligationsAlt-Ergo 1.30
VC remove_duplicate---
split_goal_right
VC remove_duplicate.00.00
VC remove_duplicate.10.00
VC remove_duplicate.20.01
VC remove_duplicate.30.00
VC remove_duplicate.40.00
VC remove_duplicate.50.00
VC remove_duplicate.60.00
VC remove_duplicate.70.00
VC remove_duplicate.80.00
VC remove_duplicate.90.00
VC remove_duplicate.100.00
VC remove_duplicate.110.00
VC remove_duplicate.120.01
VC remove_duplicate.130.01
VC remove_duplicate.140.01
VC remove_duplicate.150.04
VC remove_duplicate.160.03
VC remove_duplicate.170.02
VC remove_duplicate.180.02
VC remove_duplicate.190.02
VC remove_duplicate.200.00
VC remove_duplicate.210.00
VC remove_duplicate.220.01
VC remove_duplicate.230.00
VC remove_duplicate.240.01
VC remove_duplicate.250.02
VC remove_duplicate.260.00
VC remove_duplicate.270.00