(* Dijkstra's Dutch national flag problem
This program sorts an array where elements only have three possible values
(blue, white, and red).
Questions:
1. Prove safety (no array access out of bounds).
2. Prove termination.
3. Show that after execution the array contents is as follows:
+--------+---------+-------+
| blue | white | red |
+--------+---------+-------+
A predicate "monochrome" is provided to do so.
4. Show that after execution the array contents is a permutation of its
initial contents. Use the library predicate "permut" to do so
(the corresponding module is already loaded).
*)
module DutchNationalFlag
use import int.Int
use import ref.Ref
use import array.Array
use import array.ArrayPermut
type color = Blue | White | Red
predicate monochrome (a: array 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)
requires { true }
ensures { true }
=
let v = a[i] in
begin
a[i] <- a[j];
a[j] <- v
end
let dutch_flag (a: array color)
requires { 0 <= length a }
ensures { true }
=
let b = ref 0 in
let i = ref 0 in
let r = ref (length a) in
while !i < !r do
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
end
(*
Local Variables:
compile-command: "why3ide exo_flag.mlw"
End:
*)