#include "arrays.pi"

@pre  true
@post sorted(rv, 0, length(rv) - 1)
int[] MergeSort(int[] a)
{
  return ms(a, 0, length(a) - 1);
}

@pre  true
@post true
int[] ms(int[] a, int l, int u)
declare
  int m;
{
  if (l >= u) {
    return a;
  }
  else {
    m = (l + u) div 2;
    a = ms(a, l, m);
    a = ms(a, m + 1, u);
    a = merge(a, l, m, u);
    return a;
  }
}

@pre  true
@post true
int[] merge(int[] a, int l, int m, int u)
declare
  int i, j, k;
  int[] buf;
{
  buf = new int[u - l + 1];
  i = l;
  j = m + 1;

  for 
    @ true
    (k = 0; k < length(buf); k = k + 1)
  {
    if (i > m) {
      buf[k] = a[j];
      j = j + 1;
    }
    else if (j > u) {
      buf[k] = a[i];
      i = i + 1;
    }
    else if (a[i] <= a[j]) {
      buf[k] = a[i];
      i = i + 1;
    }
    else {
      buf[k] = a[j];
      j = j + 1;
    }
  }

  for 
    @ true
    (k = 0; k < length(buf); k = k + 1)
  {
    a[l + k] = buf[k];
  }

  return a;
}