Wiki Agenda Contact Version française

Dijkstra's national flag (variant)

Variant with number of occurrences instead of predicate permut


Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure

Tools: Why3

see also the index (by topic, by tool, by reference, by year)



Dijkstra's "Dutch national flag"

Variant with number of occurrences instead of predicate permut

module Flag

  use import int.Int
  use import map.Map
  use import ref.Ref

  type color = Blue | White | Red

  predicate monochrome (a:map int color) (i:int) (j:int) (c:color) =
    forall k:int. i <= k < j -> a[k]=c

  function nb_occ (a:map int color) (i:int) (j:int) (c:color) : int

  axiom nb_occ_null:
    forall a:map int color, i j:int, c:color.
       i >= j -> nb_occ a i j c = 0

  axiom nb_occ_add_eq:
    forall a:map int color, i j:int, c:color.
       i < j /\ get a (j-1) = c -> nb_occ a i j c = nb_occ a i (j-1) c + 1

  axiom nb_occ_add_neq:
    forall a:map int color, i j:int, c:color.
       i < j /\ get a (j-1) <> c -> nb_occ a i j c = nb_occ a i (j-1) c

  lemma nb_occ_split:
    forall a:map int color, i j k:int, c:color.
       i <= j <= k ->
         nb_occ a i k c = nb_occ a i j c + nb_occ a j k c

  lemma nb_occ_ext:
    forall a1 a2:map int color, i j:int, c:color.
       (forall k:int. i <= k < j -> get a1 k = get a2 k) ->
         nb_occ a1 i j c = nb_occ a2 i j c

  lemma nb_occ_store_outside_up:
    forall a:map int color, i j k:int, c:color.
      i <= j <= k -> nb_occ (set a k c) i j c = nb_occ a i j c

  lemma nb_occ_store_outside_down:
    forall a:map int color, i j k:int, c:color.
      k < i <= j -> nb_occ (set a k c) i j c = nb_occ a i j c

  lemma nb_occ_store_eq_eq:
    forall a:map int color, i j k:int, c:color.
      i <= k < j -> get a k = c ->
       nb_occ (set a k c) i j c = nb_occ a i j c

  lemma nb_occ_store_eq_neq:
    forall a:map int color, i j k:int, c:color.
      i <= k < j -> get a k <> c ->
       nb_occ (set a k c) i j c = nb_occ a i j c + 1

  lemma nb_occ_store_neq_eq:
    forall a:map int color, i j k:int, c c':color.
      i <= k < j -> c <> c' -> get a k = c ->
       nb_occ (set a k c') i j c = nb_occ a i j c - 1

  lemma nb_occ_store_neq_neq:
    forall a:map int color, i j k:int, c c':color.
      i <= k < j -> c <> c' -> get a k <> c ->
       nb_occ (set a k c') i j c = nb_occ a i j c

 let swap (a:ref (map int color)) (i:int) (j:int) : unit
   ensures { get !a i = get (old !a) j }
   ensures { get !a j = get (old !a) i }
   ensures { forall k:int. k <> i /\ k <> j -> get !a k = get (old !a) k }
   ensures { forall k1 k2:int, c:color. k1 <= i < k2 /\ k1 <= j < k2 ->
        nb_occ !a k1 k2 c = nb_occ (old !a) k1 k2 c }
 = let ai = get !a i in
   let aj = get !a j in
   a := set !a i aj;
   a := set !a j ai

 let dutch_flag (a:ref (map int color)) (n:int) =
    requires { 0 <= n }
    ensures { (exists b:int. exists r:int.
        monochrome !a 0 b Blue /\
        monochrome !a b r White /\
        monochrome !a r n Red) }
    ensures { forall c:color. nb_occ !a 0 n c = nb_occ (old !a) 0 n c }
  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 {
      forall c:color. nb_occ !a 0 n c = nb_occ (at !a 'Init) 0 n c }
    variant { !r - !i }
    match get !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