Какой инвариант я пропускаю в доказательстве BubbleSort?

Question

Я думаю, мне могут понадобиться дополнительные инварианты, чтобы убедить Дафни, что код работает.Я попробовал несколько, но не смог пройти.

method BubbleSort(arr: array<int>)
    ensures forall k, k' :: 0 <= k < k' < arr.Length ==> arr[k] <= arr[k']
    modifies arr
{
    var i := arr.Length;
    while i > 0
        invariant 0 <= i <= arr.Length
        // Violating the invariant next line
        invariant forall k, k' :: i <= k < k' < arr.Length ==> arr[k] <= arr[k']
        decreases i
    {
        var j := 0;
        while j < i - 1
            invariant 0 <= j < i
            invariant forall k :: 0 <= k < j ==> arr[j] >= arr[k]
            decreases i - j
        {
            if arr[j] > arr[j+1] {
                arr[j], arr[j+1] := arr[j+1], arr[j];
            }
            j := j + 1;
        }
        i := i - 1;
    }
}

Answer 1

Сортированный инвариант (a, i, a. Длина -1) должен сохраняться при уменьшении i.Инвариант partioned (a, i) гарантирует это, поскольку он подразумевает a [i-1] <= a [i].Причина, по которой он сильнее этого, заключается в том, что в противном случае его инвариантность не может быть доказана. </p>

Примечание: разделенный (a, i) говорит, что a [k] <= a [l] для всех k <= iи я <л.</p>

Answer 2

Я обнаружил среди этих заметок этот пример проверенной сортировки пузырьков.

https://www.cs.cmu.edu/~mfredrik/15414/lectures/17-notes.pdf

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

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

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

}