## Removing duplicate elements in an array, using a mutable set

Auteurs: Jean-Christophe Filliâtre

Catégories: Array Data Structure

Outils: 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 }
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
r[!j] <- a[i];
incr j
end
done;
r

end
```