1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
(** Dijkstra's "Dutch national flag" *)
module Flag
use int.Int
use ref.Ref
use array.Array
use array.ArraySwap
use 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
(* We scan the array from left to right using [i] and we maintain
the following invariant, using indices [b] and [r]:
0 b i r
+---------+----------+-----------+-------+
| Blue | White | ? | Red |
+---------+----------+-----------+-------+
*)
let dutch_flag (a:array color) : unit
ensures { exists b r: int.
monochrome a 0 b Blue /\
monochrome a b r White /\
monochrome a r (length a) Red }
ensures { permut_all (old a) a }
=
let b = ref 0 in
let i = ref 0 in
let r = ref (length a) in
while !i < !r do
invariant { 0 <= !b <= !i <= !r <= length a }
invariant { monochrome a 0 !b Blue }
invariant { monochrome a !b !i White }
invariant { monochrome a !r (length a) Red }
invariant { permut_all (old a) a }
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
|
