muller.mlw 797 Bytes
Newer Older
Jean-Christophe's avatar
Jean-Christophe committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14

module Muller

  use import int.Int
  use import module stdlib.Refint
  use import module stdlib.Array

  type param = map int
  logic pr (a : param) (n : int) = a[n] <> 0
  clone import int.NumOfParam with type param = param, logic pr = pr

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

end

(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. examples/programs/muller.gui"
End: 
*)