examples/mex.mlw

   1
   2 (** {1 Minimum excludant, aka mex}
   3
   4    Author: Jean-Christophe Filliâtre (CNRS)
   5
   6    Given a finite set of integers, find the smallest nonnegative integer
   7    that does not belong to this set.
   8
   9    In the following, the set is given as an array A.
  10    If N is the size of this array, it is clear that we have 0 <= mex <= N
  11    for we cannot have the N+1 first natural numbers in the N cells of
  12    array A (pigeon hole principle).
  13 *)
  14
  15 (**
  16    A simple algorithm is thus to mark values that belong to [0..N[ in
  17    some external Boolean array of length N, ignoring any value that is
  18    negative or greater or equal than N. Then a second loop scans the
  19    marks until we find some unused value. If don't find any, then it means
  20    that A contains exactly the integers 0,...,N-1 and the answer is N.
  21
  22    The very last step in this reasoning requires to invoke the pigeon hole
  23    principle (imported from the standard library).
  24
  25    Time O(N) and space O(N).
  26 *)
  27 module MexArray
  28
  29   use int.Int
  30   use map.Map
  31   use array.Array
  32   use ref.Refint
  33   use pigeon.Pigeonhole
  34
  35   predicate mem (x: int) (a: array int) =
  36     exists i. 0 <= i < length a && a[i] = x
  37
  38   let mex (a: array int) : int
  39     ensures { 0 <= result <= length a }
  40     ensures { not (mem result a) }
  41     ensures { forall x. 0 <= x < result -> mem x a }
  42   = let n = length a in
  43     let used = make n false in
  44     let ghost idx = ref (fun i -> i) in (* the position of each marked value *)
  45     for i = 0 to n - 1 do
  46       invariant { forall x. 0 <= x < n -> used[x] ->
  47                     mem x a && 0 <= !idx x < n && a[!idx x] = x }
  48       invariant { forall j. 0 <= j < i -> 0 <= a[j] < n ->
  49                     used[a[j]] && 0 <= !idx a[j] < n && a[!idx a[j]] = a[j] }
  50       let x = a[i] in
  51       if 0 <= x && x < n then begin used[x] <- true; idx := set !idx x i end
  52     done;
  53     let r = ref 0 in
  54     let ghost posn = ref (-1) in
  55     while !r < n && used[!r] do
  56       invariant { 0 <= !r <= n }
  57       invariant { forall j. 0 <= j < !r -> used[j] && 0 <= !idx j < n }
  58       invariant { if !posn >= 0 then 0 <= !posn < n && a[!posn] = n
  59                                 else forall j. 0 <= j < !r -> a[j] <> n }
  60       variant   { n - !r }
  61       if a[!r] = n then posn := !r;
  62       incr r
  63     done;
  64     (* we cannot have !r=n (all values marked) and !posn>=0 at the same time *)
  65     if !r = n && !posn >= 0 then pigeonhole (n+1) n (set !idx n !posn);
  66     !r
  67
  68 end
  69
  70 (**
  71   In this second implementation, we assume we are free to mutate array A.
  72
  73   The idea is then to scan the array from left to right, while
  74   swapping elements to put any value in 0..N-1 at its place in the
  75   array.  When we are done, a second loop looks for the mex, advancing
  76   as long as a[i]=i holds.
  77
  78   Since we perform only swaps, it is obvious that the mex of the final
  79   array is equal to the mex of the original array.
  80
  81   Time O(N) and space O(1). The argument for a linear time complexity is as
  82   follows: whenever we do not advance, we swap the element to its place,
  83   which is further and did not contain that element; so we can do this only
  84   N times. Note that the variant below is bounded by 2N and thus shows
  85   the linear complexity.
  86
  87   Surprinsingly, proving that N is the answer whenever array A contains a
  88   permutation of 0..N-1 is now easy (no need for a pigeon hole
  89   principle or any kind of proof by induction).
  90  *)
  91 module MexArrayInPlace
  92
  93   use int.Int
  94   use int.NumOf
  95   use array.Array
  96   use array.ArraySwap
  97   use ref.Refint
  98
  99   predicate mem (x: int) (a: array int) =
 100     exists i. 0 <= i < length a && a[i] = x
 101
 102   function placed (a: array int) : int -> bool =
 103     fun i -> a[i] = i
 104
 105   let mex (a: array int) : int
 106     ensures { 0 <= result <= length a }
 107     ensures { not (mem result (old a)) }
 108     ensures { forall x. 0 <= x < result -> mem x (old a) }
 109   = let n = length a in
 110     let i = ref 0 in
 111     while !i < n do
 112       invariant { 0 <= !i <= n }
 113       invariant { forall x. mem x a <-> mem x (old a) }
 114       invariant { forall j. 0 <= j < !i -> 0 <= a[j] < n -> a[a[j]] = a[j] }
 115       variant   { n - !i + n - numof (placed a) 0 n }
 116       let x = a[!i] in
 117       if x < 0 || x >= n || a[x] = x then
 118         incr i
 119       else if x < !i then begin
 120         swap a !i x; incr i
 121       end else
 122         swap a !i x
 123     done;
 124     assert { forall j. 0 <= j < n -> let x = (old a)[j] in
 125              0 <= x < n -> a[x] = x };
 126     for i = 0 to n - 1 do
 127       invariant { forall j. 0 <= j < i -> a[j] = j }
 128       if a[i] <> i then return i
 129     done;
 130     n
 131
 132 end
 133