include "arrays.why"

(** Selection sort *)

parameter t : int array

let selection () =
  { array_length(t) >= 1 }
  begin
    init:
    let i = ref 0 in
    while !i < (array_length_ t)-1 do
      (* t[0..i-1] is already sorted *)
      { invariant 0 <= i <= array_length(t)-1 and
	          sorted_array(t, 0, i-1) and permutation(t, t@init) and
	          forall k,l:int. 0 <= k < i ->
		    i <= l < array_length(t) -> t[k] <= t[l]
	variant array_length(t) - i }
      (* we look for the minimum of t[i..n-1] *)
      let min = ref !i in 
      let j = ref !i + 1 in
      begin
	while !j < (array_length_ t) do
	  { invariant i+1 <= j <= array_length(t) and 
	              i <= min < array_length(t) and
	              forall k:int. i <= k < j -> t[min] <= t[k]
            variant array_length(t) - j }
	  if t[!j] < t[!min] then min := !j;
	  j := !j + 1
	done;
	(* we swap t[i] and t[min] *)
	let w = t[!min] in begin t[!min] := t[!i]; t[!i] := w end
      end;
      i := !i + 1
    done
  end
  { sorted_array(t, 0, array_length(t)-1) and permutation(t, t@) }

(*
Local Variables: 
compile-command: "gwhy-bin -split-user-conj selection.mlw"
End: 
*)