## Check an array of integers for duplicate values

Topics: Array Data Structure

Tools: Why3

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

Check an array of integers for duplicate values, using the fact that values are in interval [0,m-1].

Authors: Jean-Christophe Filliâtre (CNRS) Martin Clochard (École Normale Supérieure)

```module AllDistinct

use int.Int
use ref.Ref
use array.Array

exception Duplicate

let all_distinct (a: array int) (m: int) : bool
requires { 0 <= m }
requires { forall i: int. 0 <= i < length a -> 0 <= a[i] < m }
ensures  { result <-> forall i j: int. 0 <= i < length a ->
0 <= j < length a -> i <> j -> a[i] <> a[j] }
=
let dejavu = Array.make m False in
try
for k = 0 to Array.length a - 1 do
invariant { forall i j: int. 0 <= i < k ->
0 <= j < k -> i <> j -> a[i] <> a[j] }
invariant { forall x: int. 0 <= x < m ->
dejavu[x] <-> exists i: int. 0 <= i < k /\ a[i] = x }
let v = a[k] in
if dejavu[v] then raise Duplicate;
dejavu[v] <- True
done;
True
with Duplicate ->
False
end

end
```