## 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 import int.Int
use import ref.Ref
use import 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
```

download ZIP archive

# Why3 Proof Results for Project "all_distinct"

## Theory "all_distinct.AllDistinct": fully verified in 0.00 s

 Obligations Alt-Ergo (0.99.1) 1. VC for all_distinct --- split_goal_wp 1. array creation size 0.02 2. postcondition 0.01 3. loop invariant init 0.02 4. loop invariant init 0.02 5. index in array bounds 0.02 6. type invariant 0.02 7. index in array bounds 0.01 8. postcondition 0.01 9. index in array bounds 0.02 10. loop invariant preservation 0.02 11. loop invariant preservation 0.02 12. postcondition 0.02