Mergesort correctness proof in dafny

method MergeSort(a1:array<int>) returns (a:array<int>)
  requires a1 != null && a1.Length > 0;
  ensures a != null;
  ensures forall k:: forall l:: 0 <= k < l < a.Length ==> a[k] <= a[l];
{
  a := ms(a1, 0, a1.Length-1);
  return;
}

method ms(a1:array<int>, l:int, u:int) returns (a:array<int>)
requires a1 != null && a1.Length > 0
requires 0 <= l <= u < a1.Length
ensures a != null && a.Length == a1.Length
ensures forall x:: forall y:: l <= x < y <= u ==> a[x] <= a[y];
decreases u-l;
{
  a := new int[a1.Length];
  assume forall k:: 0 <= k < a1.Length ==> a[k] == a1[k];
  if (l >= u)
  {
    return;
  }
  else
  {
    var m:int := (l + u) / 2;
    a := ms(a, l, m);
    a := ms(a, m+1, u);
    a := merge(a, l, m, u);
    return;
  }
}

method merge(a1:array<int>, l:int, m:int, u:int) returns (a:array<int>)
requires a1 != null && a1.Length > 1
requires 0 <= l <= m < u < a1.Length
requires forall x, y:: l <= x < y <= m ==> a1[x] <= a1[y]
requires forall x, y:: m+1 <= x < y <= u  ==> a1[x] <= a1[y]
ensures a != null && a.Length == a1.Length
ensures forall x,y:: l <= x < y <= u ==> a[x] <= a[y]
{
  a := new int[a1.Length];
  assume forall k:: 0 <= k < a1.Length ==> a[k] == a1[k];
  var buf := new int[u-l+1];
  var i:int := l;
  var j:int := m + 1;
  var k:int := 0;
  assert(j == m+1);
  assert(i == l);
  while (k < u-l+1)
  invariant 0 <= k <= u-l+1
  invariant k == (i-l)+(j-m-1)
  invariant 0 <= l <= m < u < a.Length
  invariant m <= j-1 <= u
  invariant l <= i <= m + 1
  invariant  forall x,y:: i <= x <= m && 0 <= y < k < u-l+1 ==> buf[y] <= a[x]
  invariant  forall x,y:: j <= x <= u && 0 <= y < k < u-l+1 ==> buf[y] <= a[x]
  invariant  forall x, y:: 0 <= x < y < k < u-l+1 ==> buf[x] <= buf[y]
  {
    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;
    }
    k := k + 1;
  }

  k := 0;
  while (k < u-l+1)
  invariant 0 <= k <= u-l+1
  invariant 0 <= l <= u < a.Length
  {
    a[l + k] := buf[k];
    k := k + 1;
  }
}