muller.mlw 837 Bytes
Newer Older
Jean-Christophe's avatar
Jean-Christophe committed
1

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
2 3 4 5 6 7
(* 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. *)

Jean-Christophe's avatar
Jean-Christophe committed
8 9 10
module Muller

  use import int.Int
11 12
  use import ref.Refint
  use import array.Array
13
  use int.NumOf as N
Jean-Christophe's avatar
Jean-Christophe committed
14

15
  function numof (a: array int) (l u: int) : int =
16
    N.numof (fun i -> a[i] <> 0) l u
Jean-Christophe's avatar
Jean-Christophe committed
17

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
18
  let compact (a: array int) =
Jean-Christophe's avatar
Jean-Christophe committed
19
    let count = ref 0 in
20
    for i = 0 to length a - 1 do
21
      invariant { 0 <= !count = numof a 0 i <= i}
Jean-Christophe's avatar
Jean-Christophe committed
22 23 24 25 26
      if a[i] <> 0 then incr count
    done;
    let u = make !count 0 in
    count := 0;
    for i = 0 to length a - 1 do
27
      invariant { 0 <= !count = numof a 0 i <= i }
28
      if a[i] <> 0 then begin u[!count] <- a[i]; incr count end
29
    done
Jean-Christophe's avatar
Jean-Christophe committed
30 31

end