Commit 541a37b4 authored by Jean-Christophe's avatar Jean-Christophe

muller's spec made even simpler

parent 0644836a
......@@ -12,13 +12,13 @@ module Muller
let compact (a : array int) =
let count = ref 0 in
for i = 0 to length a - 1 do
invariant { 0 <= count <= i and count = num_of a 0 i }
invariant { 0 <= count = num_of a 0 i <= 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 { 0 <= count <= i and count = num_of a 0 i and
invariant { 0 <= count = num_of a 0 i <= i and
length u = num_of a 0 (length a) }
if a[i] <> 0 then begin u[!count <- a[i]]; incr count end
done
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment