How to prove Loop Invariants in insertion?

Question

I'm having trouble with writing the proper loop invariants for my insertion sort algorithm listed below. I am trying to prove that all items in the array before the current index is already sorted as insertion sort is supposed to do but Dafny is not recognizing my invariants properly.

method Sort(a : array<int>)
    modifies a
    ensures forall i,j :: 0 <= i < j <  a.Length ==> a[i] <= a[j]
{
    var i := 0;
    while (i < a.Length)
    invariant 0 <= i <= a.Length
    invariant forall x,y :: 0 <= x < y < i ==> a[x] <= a[y]
    {
        var j := i - 1;
        while (j >= 0 && a[j] > a[j + 1])
        invariant forall k,l :: 0 <= k < l <i ==> a[k] <= a[l]
        {
            a[j], a[j + 1] := a[j + 1], a[j];
            j := j - 1;
        }
        i := i + 1;
    }
}

I've tried asserting that a[j] <= a[j+1] outside the loop but Dafny doesn't seem to think it's true despite it working fine inside of the loop after the swap. When I try using numbers outside the loop such as a[0] <= a[1], it doesn't verify either and I'm not sure why.

Answer 1

Your inner loop invariant doesn't seem right to me. During iteration, it does not hold. For example take following snapshot during insertion sort.

  i = 3
  j = 1
  init arr = [5, 4, 3, 2, 1]
  arr at start of inner loop = [3, 4, 5, 2, 1]
  curr arr = [3, 4, 2, 5, 1]

You need certain book keeping facts so that it can verify. Let's say that you are inserting element at i, into [0..(i-1)]. Consider extended slice [0..i], this slice is sorted unless we are comparing with element we are currently inserting. First invariant captures this. Second invariant which need to be maintained is, assuming number currently being inserted is at index j, slice [j..i] is sorted.

method sort(a: array<int>)
  modifies a
  ensures forall i, j :: 0 <= i < j < a.Length ==>  a[i] <= a[j]
{
  var i := 0;
  while i < a.Length
    invariant 0 <= i <= a.Length
    invariant forall m, n :: 0 <= m < n < i ==>  a[m] <= a[n]
  {
    var j := i - 1;
    while j >= 0 && a[j] > a[j+1]
      invariant -1 <= j <= i - 1
      invariant forall m, n :: 0 <= m < n <= i && ((m != j + 1) && (n != j + 1)) ==>  a[m] <= a[n]
      invariant forall m :: j < m <= i ==>  a[j+1] <= a[m]
    {
      a[j], a[j+1] := a[j+1], a[j];
      j := j - 1;
    }
    i := i + 1;
  }
}