why3/examples/muller.mlw

(* A small verification challenge proposed by Peter Müller.

   Given an array of integers, we first count how many non-zero values
   it contains. Then we allocate a new array with exactly this size and
   we fill it with the non-zero values. *)

module Muller

  use int.Int
  use ref.Refint
  use array.Array
  use int.NumOf as N

  function numof (a: array int) (l u: int) : int =
    N.numof (fun i -> a[i] <> 0) l u

  let compact (a: array int) =
    let count = ref 0 in
    for i = 0 to length a - 1 do
      invariant { !count = numof a 0 i }
      if a[i] <> 0 then incr count
    done;
    let u = make !count 0 in
    count := 0;
    for i = 0 to length a - 1 do
      invariant { !count = numof a 0 i }
      if a[i] <> 0 then begin u[!count] <- a[i]; incr count end
    done

end