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 2.0.0 |
VC for all_distinct | 0.06 |