Commit 4a19af9b authored by Jean-Christophe's avatar Jean-Christophe

new program example: muller

parent 1a9615d9
......@@ -367,7 +367,7 @@ install_local: bin/why3ml
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
power mergesort_list mac_carthy isqrt insertion_sort_list flag \
distance \
distance muller \
vstte10_aqueue vstte10_inverting vstte10_max_sum \
vstte10_queens vstte10_search_list \
vacid_0_sparse_array
......
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
invariant { 0 <= count <= i and count = num_of 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 { 0 <= count <= i and count = num_of a 0 i and
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:
*)
......@@ -162,6 +162,10 @@ theory NumOfParam
forall p : param, a b : int.
(forall n : int. a <= n < b -> not pr p n) -> num_of p a b = 0
lemma num_of_strictly_increasing:
forall p : param, i j k l : int.
i <= j <= k < l -> pr p k -> num_of p i j < num_of p i l
end
theory NumOf
......
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