examples/flag2.mlw

   1 (** {1 Dijkstra's "Dutch national flag"}
   2
   3   Variant with number of occurrences instead of predicate [permut]
   4
   5 *)
   6
   7 module Flag
   8
   9   use int.Int
  10   use map.Map
  11   use ref.Ref
  12
  13   type color = Blue | White | Red
  14
  15   let eq_color (c1 c2 :color) : bool
  16     ensures { result <-> c1 = c2 }
  17   = match c1,c2 with
  18     | Blue,Blue | Red,Red | White,White -> True
  19     | _,_ -> False
  20     end
  21
  22   predicate monochrome (a: map int color) (i: int) (j: int) (c: color) =
  23     forall k: int. i <= k < j -> a[k]=c
  24
  25   let rec function nb_occ (a: map int color) (i: int) (j: int) (c: color) : int
  26     variant { j - i }
  27   = if i >= j then 0 else
  28     if eq_color a[j-1] c then 1 + nb_occ a i (j-1) c else nb_occ a i (j-1) c
  29
  30   let rec lemma nb_occ_split (a: map int color) (i j k: int) (c: color)
  31     requires { i <= j <= k }
  32     variant { k - j }
  33     ensures { nb_occ a i k c = nb_occ a i j c + nb_occ a j k c }
  34   = if k = j then () else nb_occ_split a i j (k-1) c
  35
  36   let rec lemma nb_occ_ext (a1 a2: map int color) (i j: int) (c: color)
  37     requires { forall k: int. i <= k < j -> a1[k] = a2[k] }
  38     variant { j - i }
  39     ensures { nb_occ a1 i j c = nb_occ a2 i j c }
  40   = if i >= j then () else nb_occ_ext a1 a2 i (j-1) c
  41
  42   lemma nb_occ_store_outside_up:
  43     forall a: map int color, i j k: int, c: color.
  44       i <= j <= k -> nb_occ (set a k c) i j c = nb_occ a i j c
  45
  46   lemma nb_occ_store_outside_down:
  47     forall a: map int color, i j k: int, c: color.
  48       k < i <= j -> nb_occ (set a k c) i j c = nb_occ a i j c
  49
  50   lemma nb_occ_store_eq_eq:
  51     forall a: map int color, i j k: int, c: color.
  52       i <= k < j -> a[k] = c ->
  53        nb_occ (set a k c) i j c = nb_occ a i j c
  54
  55   let rec lemma nb_occ_store_eq_neq (a: map int color) (i j k: int) (c: color)
  56     requires { i <= k < j }
  57     requires { a[k] <> c }
  58     variant  { j - k }
  59     ensures  { nb_occ (set a k c) i j c = nb_occ a i j c + 1 }
  60   = if k = j - 1 then () else nb_occ_store_eq_neq a i (j-1) k c
  61
  62   let lemma nb_occ_store_neq_eq
  63     (a: map int color) (i j k: int) (c c': color)
  64     requires { i <= k < j } requires { c <> c' } requires { a[k] = c }
  65     ensures  { nb_occ (set a k c') i j c = nb_occ a i j c - 1 }
  66   = nb_occ_split a i k j c; nb_occ_split (set a k c') i k j c;
  67     nb_occ_split a k (k + 1) j c; nb_occ_split (set a k c') k (k+1) j c
  68
  69   let lemma nb_occ_store_neq_neq
  70     (a: map int color) (i j k: int) (c c': color)
  71     requires { i <= k < j } requires { c <> c' } requires { a[k] <> c }
  72     ensures  { nb_occ (set a k c') i j c = nb_occ a i j c }
  73   = nb_occ_split a i k j c; nb_occ_split (set a k c') i k j c;
  74     nb_occ_split a k (k + 1) j c; nb_occ_split (set a k c') k (k+1) j c
  75
  76   use array.Array
  77
  78  let swap (a:array color) (i: int) (j: int) : unit
  79    requires { 0 <= i < a.length }
  80    requires { 0 <= j < a.length }
  81    ensures { a[i] = old a[j] }
  82    ensures { a[j] = old a[i] }
  83    ensures { forall k: int. k <> i /\ k <> j -> a[k] = old a[k] }
  84    ensures { forall k1 k2: int, c: color. k1 <= i < k2 /\ k1 <= j < k2 ->
  85         nb_occ a.elts k1 k2 c = nb_occ (old a.elts) k1 k2 c }
  86  = let ai = a[i] in
  87    let aj = a[j] in
  88    a[i] <- aj;
  89    a[j] <- ai
  90
  91
  92  let dutch_flag (a:array color)
  93     ensures { (exists b: int. exists r: int.
  94         monochrome a.elts 0 b Blue /\
  95         monochrome a.elts b r White /\
  96         monochrome a.elts r a.length Red) }
  97     ensures { forall c: color.
  98         nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c }
  99 = let b = ref 0 in
 100   let i = ref 0 in
 101   let r = ref a.length in
 102   while !i < !r do
 103     invariant { 0 <= !b <= !i <= !r <= a.length }
 104     invariant { monochrome a.elts 0 !b Blue }
 105     invariant { monochrome a.elts !b !i White }
 106     invariant { monochrome a.elts !r a.length  Red }
 107     invariant {
 108       forall c: color.
 109         nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c }
 110     variant { !r - !i }
 111     match a[!i] with
 112     | Blue -> swap a !b !i; b := !b + 1; i := !i + 1
 113     | White -> i := !i + 1
 114     | Red -> r := !r - 1; swap a !r !i
 115     end
 116   done
 117
 118 end