(* Dijkstra's "Dutch national flag"
The following program sorts an array whose elements may have three
different values, standing for the three colors of the Dutch
national flag (blue, white, and red).
Questions:
1. Prove safety i.e. the absence of array access out of bounds.
2. Prove termination.
3. Prove that, after execution, the array is sorted as follows:
+--------+---------+---------+
| blue | white | red |
+--------+---------+---------+
(using the predicate "monochrome" that is provided).
4. Show that after execution the array contents is a permutation of its
initial contents. Use the library predicate "permut_all" to do so
(the corresponding module ArrayPermut is already imported).
*)
module Flag
use import int.Int
use import ref.Ref
use import array.Array
use import array.ArraySwap
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 dutch_flag (a: array color)
requires { 0 <= length a }
=
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: "why3 ide exo_flag.mlw"
End:
*)