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 int.Int use map.Map use ref.Ref type color = Blue | White | Red let eq_color (c1 c2 :color) : bool ensures { result <-> c1 = c2 } = match c1,c2 with | Blue,Blue | Red,Red | White,White -> True | _,_ -> False end predicate monochrome (a: map int color) (i: int) (j: int) (c: color) = forall k: int. i <= k < j -> a[k]=c let rec function nb_occ (a: map int color) (i: int) (j: int) (c: color) : int 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 let rec lemma nb_occ_split (a: map int color) (i j k: int) (c: color) 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 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] } 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 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 -> a[k] = c -> nb_occ (set a k c) i j c = nb_occ a i j c let rec lemma nb_occ_store_eq_neq (a: map int color) (i j k: int) (c: color) requires { i <= k < j } requires { a[k] <> c } variant { j - k } ensures { nb_occ (set a k c) i j c = nb_occ a i j c + 1 } = if k = j - 1 then () else nb_occ_store_eq_neq a i (j-1) k c 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 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 use array.Array let swap (a:array color) (i: int) (j: int) : unit requires { 0 <= i < a.length } requires { 0 <= j < a.length } ensures { a[i] = old a[j] } ensures { a[j] = old a[i] } 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 -> 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 let dutch_flag (a:array color) ensures { (exists b: int. exists r: int. monochrome a.elts 0 b Blue /\ monochrome a.elts b r White /\ monochrome a.elts r a.length Red) } ensures { forall c: color. nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c } = let b = ref 0 in let i = ref 0 in let r = ref a.length in while !i < !r do 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 } invariant { forall c: color. nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c } 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
download ZIP archive