The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

## Dijkstra's national flag

Dijkstra's national flag consists in sorting an array containing only three values (namely Blue, White and Red).

Authors: Jean-Christophe Filliâtre

Topics: Sorting Algorithm

Tools: Why3

Dijkstra's "Dutch national flag"

```
module Flag

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 { 0 <= i < length a /\ 0 <= j < length a }
ensures { exchange (old a) a i j }
let v = a[i] in
begin
a[i] <- a[j];
a[j] <- v
end

let dutch_flag (a:array color) (n:int) =
requires { 0 <= n /\ length a = n }
ensures { exists b:int. exists r:int.
monochrome a 0 b Blue /\
monochrome a b r White /\
monochrome a r n Red }
ensures { permut (old a) a }
let b = ref 0 in
let i = ref 0 in
let r = ref n in
'Init:
while !i < !r do
invariant { 0 <= !b <= !i <= !r <= n }
invariant { monochrome a 0  !b Blue }
invariant { monochrome a !b !i White }
invariant { monochrome a !r n  Red }
invariant { length a = n }
invariant { permut_sub (at a 'Init) a 0 n }
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

end
```

download ZIP archive