How to prove time complexity of bubble sort using dafny?

Question

Is there a way in dafny to create an invariant specific to a single loop iteration? Below I'm trying to create a dafny program to upper bound the number of swaps of bubble sort. That value is stored in variable n. So I'd like to upper bound n by (a.Length * (a.Length - 1))/2. The reason being is that the maximum number of swaps that can occur is if the array is in the opposite order so then there must be n swaps on the first iteration of the inside loop and then n-1 swaps of the second iteration of the inside loop, etc. until the array is sorted. This is equivalent to 1+2+3+...+n-1+n = n(n-1)/2, which is precisely what I'm trying to show. I'm wondering if there's a method in dafny to upper bound the value of i-j or n in the code below based on the iteration of the inner loop. Is there such a way?

If not is there another method to upper bound this n value given the explanation provided above? Perhaps additional invariants I'm not thinking of?

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 0 < a.Length ==> 0 <= i < a.Length;
          decreases i;
           {
            var j := 0;
            while (j < i)
            invariant i - j <= old(i) - old(j);
            invariant i < 0 && j < 0 ==> 0 <= n <= a.Length;
            decreases i - j;
              {
                if(a[j] > a[j+1])
                  {
                    a[j], a[j+1] := a[j+1], a[j];
                    n := n + 1;
                  }
                  j := j + 1;
              }
              i := i -1;
          }
    }

Answer 1

I don't think you need to "create an invariant specific to a single loop iteration", but instead to rephrase your loop invariants in a way that they apply to all iterations.

Your English argument for why the complexity is bounded is a good one.

the maximum number of swaps that can occur is if [there are] n swaps on the first iteration of the inside loop and then n-1 swaps of the second iteration of the inside loop, etc. until the array is sorted. This is equivalent to 1+2+3+...+n-1+n = n(n-1)/2

All you need to do is to formalize this argument into Dafny. I suggest introducing a function for "the sum of all integers between a and b" and then using that function to phrase your loop invariants.