examples/flag.mlw

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