Дафни: Почему это утверждение не работает и как это исправить

Пытаюсь доказать простой алгоритм на Dafny, но получаю «нарушение утверждения» в последнем утверждении без дополнительных деталей. Кто-нибудь может определить, что не так и как это исправить? Формальные методы - не моя специальность.

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

predicate sorted(a: array?<int>, l: int , u: int)
    reads a //Sintaxe do Dafny. PRECISA disso para dizer que vai ler o array
    requires a != null
{
    forall i, j :: 0 <= l <= i <= j <= u < a.Length ==> a[i] <= a[j]
}

predicate partitioned(a: array?<int>, i: int)
    reads a
    requires a != null
{
    forall k, k' :: 0 <= k <= i < k' < a.Length ==> a[k] <= a[k']
}

method testSort()
{
  var b := new int[2];
  b[0], b[1] := 2, 1;
  assert b[0] == 2 && b[1] == 1;
  BubbleSort(b);
  assert b[0] == 1 && b[1] == 2;
}