ghost predicate sorted(a: array?<int>, l: int, u: int)
  reads a
  requires a != null
  {
    forall i, j :: 0 <= l <= i <= j <= u < a.Length ==> a[i] <= a[j]
  }

method BubbleSort(a: array?<int>)
  modifies a
  requires a != null
  ensures sorted(a, 0, a.Length-1)
  ensures multiset(a[..]) == old(multiset(a[..]))
  {
    var i := a.Length - 1;
    while(i > 0)
      invariant a.Length > 0 ==>  0 <= i < a.Length 
      invariant sorted(a, i, a.Length - 1)
      invariant forall l,m :: (0 <= m <= i && i < l < a.Length) ==> a[l]>=a[m]
      invariant multiset(a[..]) == old(multiset(a[..]))
       {
        var j := 0;
        while (j < i)
          invariant 0 <= j <= i
          invariant forall k :: 0 <= k < j ==> a[k] <= a[j]
          invariant sorted(a, i, a.Length - 1)
          invariant forall l,m :: (0 <= m <= i && i < l < a.Length) ==> a[l]>=a[m]
          invariant multiset(a[..]) == old(multiset(a[..]))
          {
            if(a[j] > a[j+1])
              {
                a[j], a[j+1] := a[j+1], a[j];
              }
              j := j + 1;
          }
          i := i -1;
      }
  }