new program: Dijkstra's national flag

parent e9992947
......@@ -366,7 +366,7 @@ install_local: bin/why3ml
bin/why3doc -b -o $(GALLERYDIR)/`basename $*` $*.mlw
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
power mergesort_list mac_carthy isqrt insertion_sort_list \
power mergesort_list mac_carthy isqrt insertion_sort_list flag \
vstte10_aqueue \
vstte10_inverting \
vstte10_max_sum \
......
(** Dijkstra's "Dutch national flag" *)
module Flag
use import int.Int
use import module stdlib.Ref
use import module stdlib.Array
use import array.ArrayPermut
type color = Blue | White | Red
logic monochrome (a:map color) (i:int) (j:int) (c:color) =
forall k:int. i<=k<j -> a[k]=c
let swap (a:array color) (i:int) (j:int) =
{ 0 <= i < length a and 0 <= j < length a }
let v = a[i] in
begin
a[i <- a[j]];
a[j <- v]
end
{ exchange a (old a) i j }
let dutch_flag (a:array color) (n:int) =
{ 0 <= n and length a = n }
let b = ref 0 in
let i = ref 0 in
let r = ref n in
label Init:
while !i < !r do
invariant { 0 <= b <= i and i <= r <= n and
monochrome a 0 b Blue and
monochrome a b i White and
monochrome a r n Red and
length a = n and
permut a (at a Init) 0 (n-1) }
variant { r - i }
match a[!i] with
| Blue ->
swap a !b !i;
b := !b + 1;
i := !i + 1
| White ->
i := !i + 1
| Red ->
r := !r - 1;
swap a !r !i
end
done
{ (exists b:int. exists r:int.
monochrome a 0 b Blue and
monochrome a b r White and
monochrome a r n Red)
and permut a (old a) 0 (n-1) }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/flag.gui"
End:
*)
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