(** Fully axiomatic version of Dijkstra's "Dutch national flag" 
    See also flag.mlw in the same directory *)

type color

logic blue : color
logic white : color
logic red : color

predicate is_color(c:color) = c=blue or c=white or c=red

parameter eq_color  : 
  c1:color -> c2:color -> {} bool { if result then c1=c2 else c1<>c2 }

type color_array

logic acc : color_array, int -> color
logic upd : color_array, int, color -> color_array
logic length : color_array -> int

axiom acc_upd_eq :
  forall a:color_array. forall i:int. forall c:color.
    acc(upd(a,i,c),i) = c

axiom acc_upd_neq :
  forall a:color_array. forall i,j:int. forall c:color.
    i <> j -> acc(upd(a,j,c),i) = acc(a,i)

axiom length_update : 
  forall a:color_array. forall i:int. forall c:color.
    length(upd(a,i,c)) = length(a)

parameter get : 
  t:color_array ref -> i:int -> 
    { 0<=i<length(t) } color reads t { result=acc(t,i) }

parameter set : 
  t:color_array ref -> i:int -> c:color -> 
    { 0<=i<length(t) } unit writes t { t=upd(t@,i,c) }

predicate monochrome(t:color_array, i:int, j:int, c:color) =
  forall k:int. i<=k<j -> acc(t,k)=c

logic Permutation : color_array, color_array, int, int -> prop

axiom permut_refl : forall t: color_array. forall l,r:int.
  Permutation(t,t,l,r)

axiom permut_swap : forall t:color_array. forall l,r,i,j:int.
  l <= i <= r -> l <= j <= r ->
  Permutation(t, upd(upd(t,i,acc(t,j)), j, acc(t,i)), l, r)

axiom permut_sym : forall t1,t2:color_array. forall l,r:int.
  Permutation(t1,t2,l,r) -> Permutation(t2,t1,l,r)

axiom permut_trans : forall t1,t2,t3: color_array. forall l,r:int.
  Permutation(t1,t2,l,r) -> Permutation(t2,t3,l,r) -> Permutation(t1,t3,l,r)

let swap (t:color_array ref) (i:int) (j:int) =
  { 0 <= i < length(t) and 0 <= j < length(t) }
  let u = get t i in
  set t i (get t j);
  set t j u
  { t = upd(upd(t@,i,acc(t@,j)), j, acc(t@,i)) }

let dutch_flag (t:color_array ref) (n:int) = 
  { 0 <= n and length(t) = n and 
    forall k:int. 0 <= k < n -> is_color(acc(t,k)) }
  let b = ref 0 in
  let i = ref 0 in
  let r = ref n in
  init:
  while !i < !r do
     { invariant 0 <= b <= i and i <= r <= n and
	         monochrome(t,0,b,blue) and 
	         monochrome(t,b,i,white) and 
	         monochrome(t,r,n,red) and
		 length(t) = n and
                 (forall k:int. 0 <= k < n -> is_color(acc(t,k))) and
	         Permutation(t,t@init,0,n-1)
       variant r - i }
     if eq_color (get t !i) blue then begin
       swap t !b !i;
       b := !b + 1;
       i := !i + 1
     end else if eq_color (get t !i) white then
       i := !i + 1
     else begin
       r := !r - 1;
       swap t !r !i
     end
  done
  { (exists b:int. exists r:int.	
      monochrome(t,0,b,blue) and 
      monochrome(t,b,r,white) and 
      monochrome(t,r,n,red))
    and Permutation(t,t@,0,n-1) }

(*
Local Variables: 
compile-command: "gwhy flag_ax.mlw"
End: 
*)