examples/array_most_frequent.mlw

   1
   2 (** A simple programming exercise: find out the most frequent value in an array
   3
   4     Using an external table (e.g. a hash table), we can easily do it
   5     in linear time and space.
   6
   7     However, if the array is sorted, we can do it in linear time and
   8     constant space.
   9
  10     Author: Jean-Christophe Filliâtre (CNRS)
  11 *)
  12
  13 use int.Int
  14 use ref.Refint
  15 use array.Array
  16 use array.NumOfEq
  17
  18 let most_frequent (a: array int) : int
  19   requires { length a > 0 }
  20   requires { forall i j. 0 <= i <= j < length a -> a[i] <= a[j] }
  21   ensures  { numof a result 0 (length a) > 0 }
  22   ensures  { forall x. numof a x 0 (length a) <= numof a result 0 (length a) }
  23 = let ref r = a[0] in
  24   let ref c = 1 in
  25   let ref m = 1 in
  26   for i = 1 to length a - 1 do
  27     invariant { c = numof a a[i-1] 0 i }
  28     invariant { m = numof a r 0 i }
  29     invariant { forall x. numof a x 0 i <= m }
  30     if a[i] = a[i-1] then begin
  31       incr c;
  32       if c > m then begin m <- c; r <- a[i] end
  33     end else
  34       c <- 1
  35   done;
  36   r