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

Quadratic implementation, without extra space

module RemoveDuplicate

  use Spec
  use ref.Refint
  use array.Array

  type elt
  clone import set.SetImp as MutableSet with type elt = elt

  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.empty () in
    for i = 0 to Array.length a - 1 do
      invariant { forall x: elt. appears x a i <-> mem x s }
      MutableSet.add a[i] s
    done;
    label L in
    let r = Array.make (MutableSet.cardinal 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 }
      invariant { forall x: elt. mem x s <-> appears x r !j }
      invariant { nodup r !j }
      invariant { 0 <= !j = cardinal s <= length r }
      invariant { subset s (s at L) }
      if not (MutableSet.mem a[i] s) then begin
        MutableSet.add a[i] s;
        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 2.2.0CVC4 1.6Eprover 1.8-001
VC for remove_duplicate---------
split_vc
loop invariant init---0.04---
index in array bounds---0.02---
loop invariant preservation0.03------
index in array bounds---0.02---
array creation size---0.04---
loop invariant init---0.04---
loop invariant init---0.05---
loop invariant init---0.04---
loop invariant init---0.04---
loop invariant init---0.04---
index in array bounds---0.04---
index in array bounds---0.02---
index in array bounds---0.02---
index in array bounds0.02------
loop invariant preservation0.04------
loop invariant preservation0.12------
loop invariant preservation0.12------
loop invariant preservation0.02------
loop invariant preservation---0.29---
loop invariant preservation---0.41---
loop invariant preservation---0.04---
loop invariant preservation---0.02---
loop invariant preservation---0.02---
loop invariant preservation---0.02---
postcondition------0.90
postcondition------5.16
out of loop bounds---0.02---
out of loop bounds---0.05---