examples/all_distinct.mlw

   1
   2 (** Check an array of integers for duplicate values,
   3     using the fact that values are in interval [0,m-1].
   4
   5     Authors: Jean-Christophe Filliâtre (CNRS)
   6              Martin Clochard (École Normale Supérieure)
   7 *)
   8
   9 module AllDistinct
  10
  11   use int.Int
  12   use ref.Ref
  13   use array.Array
  14
  15   exception Duplicate
  16
  17   let all_distinct (a: array int) (m: int) : bool
  18     requires { 0 <= m }
  19     requires { forall i: int. 0 <= i < length a -> 0 <= a[i] < m }
  20     ensures  { result <-> forall i j: int. 0 <= i < length a ->
  21                           0 <= j < length a -> i <> j -> a[i] <> a[j] }
  22   =
  23    let dejavu = Array.make m False in
  24    try
  25      for k = 0 to Array.length a - 1 do
  26        invariant { forall i j: int. 0 <= i < k ->
  27                    0 <= j < k -> i <> j -> a[i] <> a[j] }
  28        invariant { forall x: int. 0 <= x < m ->
  29                    dejavu[x] <-> exists i: int. 0 <= i < k /\ a[i] = x }
  30        let v = a[k] in
  31        if dejavu[v] then raise Duplicate;
  32        dejavu[v] <- True
  33      done;
  34      True
  35    with Duplicate ->
  36      False
  37    end
  38
  39 end