flag2.mlw 3.9 KB
Newer Older
1 2
(** {1 Dijkstra's "Dutch national flag"}

3
  Variant with number of occurrences instead of predicate [permut]
4 5 6 7 8

*)

module Flag

9 10 11
  use int.Int
  use map.Map
  use ref.Ref
12 13 14

  type color = Blue | White | Red

MARCHE Claude's avatar
MARCHE Claude committed
15 16 17 18 19 20 21
  let eq_color (c1 c2 :color) : bool
    ensures { result <-> c1 = c2 }
  = match c1,c2 with
    | Blue,Blue | Red,Red | White,White -> True
    | _,_ -> False
    end

22 23
  predicate monochrome (a: map int color) (i: int) (j: int) (c: color) =
    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
MARCHE Claude's avatar
MARCHE Claude committed
26 27 28
    variant { j - i }
  = if i >= j then 0 else
    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)
MARCHE Claude's avatar
MARCHE Claude committed
31 32 33 34
    requires { i <= j <= k }
    variant { k - j }
    ensures { nb_occ a i k c = nb_occ a i j c + nb_occ a j k c }
  = if k = j then () else nb_occ_split a i j (k-1) c
35

36 37
  let rec lemma nb_occ_ext (a1 a2: map int color) (i j: int) (c: color)
    requires { forall k: int. i <= k < j -> a1[k] = a2[k] }
MARCHE Claude's avatar
MARCHE Claude committed
38 39 40
    variant { j - i }
    ensures { nb_occ a1 i j c = nb_occ a2 i j c }
  = if i >= j then () else nb_occ_ext a1 a2 i (j-1) c
Andrei Paskevich's avatar
Andrei Paskevich committed
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 49 50
      k < i <= j -> nb_occ (set a k c) i j c = nb_occ a i j c

  lemma nb_occ_store_eq_eq:
51
    forall a: map int color, i j k: int, c: color.
MARCHE Claude's avatar
MARCHE Claude committed
52
      i <= k < j -> a[k] = c ->
53 54
       nb_occ (set a k c) i j c = nb_occ a i j c

55
  let rec lemma nb_occ_store_eq_neq (a: map int color) (i j k: int) (c: color)
MARCHE Claude's avatar
MARCHE Claude committed
56 57
    requires { i <= k < j }
    requires { a[k] <> c }
58 59
    variant  { j - k }
    ensures  { nb_occ (set a k c) i j c = nb_occ a i j c + 1 }
MARCHE Claude's avatar
MARCHE Claude committed
60
  = if k = j - 1 then () else nb_occ_store_eq_neq a i (j-1) k c
61

62 63 64 65 66 67
  let lemma nb_occ_store_neq_eq
    (a: map int color) (i j k: int) (c c': color)
    requires { i <= k < j } requires { c <> c' } requires { a[k] = c }
    ensures  { nb_occ (set a k c') i j c = nb_occ a i j c - 1 }
  = nb_occ_split a i k j c; nb_occ_split (set a k c') i k j c;
    nb_occ_split a k (k + 1) j c; nb_occ_split (set a k c') k (k+1) j c
68

69 70 71 72 73 74
  let lemma nb_occ_store_neq_neq
    (a: map int color) (i j k: int) (c c': color)
    requires { i <= k < j } requires { c <> c' } requires { a[k] <> c }
    ensures  { nb_occ (set a k c') i j c = nb_occ a i j c }
  = nb_occ_split a i k j c; nb_occ_split (set a k c') i k j c;
    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
MARCHE Claude's avatar
MARCHE Claude committed
79 80 81 82
   requires { 0 <= i < a.length }
   requires { 0 <= j < a.length }
   ensures { a[i] = old a[j] }
   ensures { a[j] = old a[i] }
83 84
   ensures { forall k: int. k <> i /\ k <> j -> a[k] = old a[k] }
   ensures { forall k1 k2: int, c: color. k1 <= i < k2 /\ k1 <= j < k2 ->
MARCHE Claude's avatar
MARCHE Claude committed
85 86 87 88 89
        nb_occ a.elts k1 k2 c = nb_occ (old a.elts) k1 k2 c }
 = let ai = a[i] in
   let aj = a[j] in
   a[i] <- aj;
   a[j] <- ai
90 91


MARCHE Claude's avatar
MARCHE Claude committed
92
 let dutch_flag (a:array color)
93
    ensures { (exists b: int. exists r: int.
MARCHE Claude's avatar
MARCHE Claude committed
94 95 96
        monochrome a.elts 0 b Blue /\
        monochrome a.elts b r White /\
        monochrome a.elts r a.length Red) }
97
    ensures { forall c: color.
MARCHE Claude's avatar
MARCHE Claude committed
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
MARCHE Claude's avatar
MARCHE Claude committed
101
  let r = ref a.length in
102
  while !i < !r do
MARCHE Claude's avatar
MARCHE Claude committed
103 104 105 106
    invariant { 0 <= !b <= !i <= !r <= a.length }
    invariant { monochrome a.elts 0 !b Blue }
    invariant { monochrome a.elts !b !i White }
    invariant { monochrome a.elts !r a.length  Red }
107
    invariant {
108
      forall c: color.
MARCHE Claude's avatar
MARCHE Claude committed
109
        nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c }
110
    variant { !r - !i }
MARCHE Claude's avatar
MARCHE Claude committed
111
    match a[!i] with
112 113 114 115 116
    | 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
117 118

end