include "arrays.why"

axiom mean : forall l,u:int. l < u -> l <= (l+u)/2 < u

parameter merge :
  a:int array -> l:int -> m:int -> u:int ->
  { l <= m < u and sorted_array(a,l,m) and sorted_array(a,m+1,u) }
  unit writes a
  { sorted_array(a, l, u) and permut(a@, a, l, u) }

let rec mergesort (a:int array) (l:int) (u:int) : unit =
  { }
  init:
  if l < u then begin
    let m = (l+u)/2 in
    mergesort a l m;
    assert {permut(a@init, a, l, u) };
    mergesort a (m+1) u;
    merge a l m u
  end
  { sorted_array(a, l, u) and permut(a@, a, l, u) }


(*
Local Variables: 
compile-command: "gwhy mergesort.why"
End: 
*)