## Check an array of integers for duplicate values

**Authors:** Jean-Christophe Filliâtre / Martin Clochard

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

download ZIP archive

# Why3 Proof Results for Project "all_distinct"

## Theory "all_distinct.AllDistinct": fully verified

Obligations | Alt-Ergo 1.30 |

VC all_distinct | 0.06 |