Wiki Agenda Contact Version française

Check an array of integers for duplicate values


Authors: Jean-Christophe Filliâtre / Martin Clochard

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.21 s

ObligationsAlt-Ergo (0.99.1)
VC for all_distinct---
split_goal_wp
  1. array creation size0.02
2. postcondition0.01
3. loop invariant init0.02
4. loop invariant init0.02
5. index in array bounds0.02
6. type invariant0.02
7. index in array bounds0.01
8. postcondition0.01
9. index in array bounds0.02
10. loop invariant preservation0.02
11. loop invariant preservation0.02
12. postcondition0.02