method BubbleSort(a: array?<int>) returns (n: nat) 
  modifies a
  requires a != null
  ensures n <= (a.Length * (a.Length - 1))/2
{
    var i := a.Length - 1;
    n := 0;
    while (i > 0)
       invariant n <= (a.Length * (a.Length - 1) - (i * (i + 1)))/2  
       {
        var j := 0;
        assert n <= (a.Length * (a.Length - 1) - (i * (i + 1)))/2 ;
        ghost var on := n;
        while (j < i)
          invariant n <= (a.Length * (a.Length - 1) - (i * (i - 1)))/2
          invariant n <= on + j 
          {

            if(a[j] > a[j+1])
              {
                a[j], a[j+1] := a[j+1], a[j];
                n := n + 1;
              }
              j := j + 1;

            calc <= {
              n;
              on + i;
              (a.Length * (a.Length - 1) - (i * (i - 1)))/2;
            }
          }
          i := i -1;
      }
}