(* The 2nd Verified Software Competition (VSTTE 2012)
   https://sites.google.com/site/vstte2012/compet

   Problem 1:
   Sorting an array of Boolean values, using swaps only *)

module TwoWaySort

  use int.Int
  use bool.Bool
  use ref.Refint
  use array.Array
  use array.ArraySwap
  use array.ArrayPermut

  predicate le (x y: bool) = x = False \/ y = True

  predicate sorted (a: array bool) =
    forall i1 i2: int. 0 <= i1 <= i2 < a.length -> le a[i1] a[i2]

  let two_way_sort (a: array bool)
    ensures { sorted a }
    ensures { permut_all (old a) a }
  = let i = ref 0 in
    let j = ref (length a - 1) in
    while !i < !j do
      invariant { 0 <= !i /\ !j < length a }
      invariant { forall k: int. 0 <= k < !i -> a[k] = False }
      invariant { forall k: int. !j < k < length a -> a[k] = True }
      invariant { permut_all (old a) a }
      variant   { !j - !i }
      if not a[!i] then incr i
      else if a[!j] then decr j
      else begin swap a !i !j; incr i; decr j end
    done

end