## 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

 Obligations Alt-Ergo 2.2.0 CVC4 1.6 Eprover 1.8-001 VC for remove_duplicate --- --- --- split_vc loop invariant init --- 0.04 --- index in array bounds --- 0.02 --- loop invariant preservation 0.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 bounds 0.02 --- --- loop invariant preservation 0.04 --- --- loop invariant preservation 0.12 --- --- loop invariant preservation 0.12 --- --- loop invariant preservation 0.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 ---