Sort and switch methods in Dafny (Invariants error)

Question

I am new to Dafny and wrote two methods, switch and sort. In sort I get an error in line 10 and 12 and in switch in line 24 and 26. Both based on the forall invaraiants. I'm struggling and can't figure out why.

The error messages I'm getting are "this loop invariant might not be mantained by the loop".

method sort(a: array<int>)
    modifies a
    ensures forall h, k: int ::
        0 <= h < k < a.Length ==> a[h] <= a[k];
{
    var i := 0;

    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant forall h, k: int :: //error (forall)
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
        invariant forall h, k: int :: //error (error forall)
            0 <= h < k < i ==> a[h] <= a[k];
    {
        var index := i;
        var j := i+1;
        while j < a.Length
            invariant 0 <= i < j <= a.Length
            invariant 0 <= index < j
            invariant forall h, k: int ::
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
            invariant forall h, k: int ::
                0 <= h < k < i ==> a[h] <= a[k];
            invariant forall k: int ::
                i <= k < j ==> a[index] <= a[k]
        {
            if a[j] < a[index] {
                index := j;
            }
            j := j + 1;
        }

        var tmp := a[index];
        a[index] := a[i];
        a[i] := tmp;
        i := i + 1;
    }
}

method switch(a: array<int>, b: array<int>, j: int)
    modifies a
    modifies b
    requires 0 <= j <= a.Length
    requires 0 <= j <= b.Length
    ensures forall k: int ::
        (0 <= k < j ==> a[k] == old(b[k]))
    ensures forall k: int ::
        (0 <= k < j ==> b[k] == old(a[k]))
    ensures forall k: int ::
        (j <= k < b.Length ==> b[k] == old(b[k]))
    ensures forall k: int ::
        (j <= k < a.Length ==> a[k] == old(a[k]))
     
{
    var i := 0;

    while i < j
        invariant 0 <= i <= j <= a.Length;
        invariant forall k: int ::
            (j <= k < a.Length ==> a[k] == old(a[k]))
        invariant forall k: int ::
            (j <= k < b.Length ==> b[k] == old(b[k]))   
        invariant forall k: int :: // error (forall)
            (0 <= k < i ==> a[k] == old(b[k]))
        invariant forall k: int :: // error (forall)
            (0 <= k < i ==> b[k] == old(a[k]))
    {
        var tmp := b[i];
        b[i] := a[i];
        a[i] := tmp;
        i := i + 1;
        //assert a[i - 1] == old(b[i-1]);
    }
}

How can I fix this, what would be the correct invariants?

Answer 1

Let me introduce you to the almost universal technique of verification debugging introduced recently in the docs.

Let me apply it to your case. First, you get the message that the "invariant might not be maintained by the loop". So the first idea, is to move the assertion at the end of the loop, to capture this idea, like this:

method sort(a: array<int>)
    modifies a
    ensures forall h, k: int ::
        0 <= h < k < a.Length ==> a[h] <= a[k];
{
    var i := 0;

    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant forall h, k: int :: //No more error
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
        invariant forall h, k: int :: //No more error
            0 <= h < k < i ==> a[h] <= a[k];
    {
        var index := i;
        var j := i+1;
        while j < a.Length
            invariant 0 <= i < j <= a.Length
            invariant 0 <= index < j
            invariant forall h, k: int ::
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
            invariant forall h, k: int ::
                0 <= h < k < i ==> a[h] <= a[k];
            invariant forall k: int ::
                i <= k < j ==> a[index] <= a[k]
        {
            if a[j] < a[index] {
                index := j;
            }
            j := j + 1;
        }

        var tmp := a[index];
        a[index] := a[i];
        a[i] := tmp;
        i := i + 1;
        assert forall h, k: int :: //error (forall)
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
        assert forall h, k: int :: //error (error forall)
            0 <= h < k < i ==> a[h] <= a[k];
    }
}

Now, the technique of verification debugging consists of moving the assertions back through the definitions in what is called a weakest precondition calculus (mostly described practically in the link at the beginning of this post). For example, to move these assertions above the assignment i := i + 1, you'd simply replace i by i + 1 in these assertions, like this:

method sort(a: array<int>)
    modifies a
    ensures forall h, k: int ::
        0 <= h < k < a.Length ==> a[h] <= a[k];
{
    var i := 0;

    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant forall h, k: int ::
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
        invariant forall h, k: int ::
            0 <= h < k < i ==> a[h] <= a[k];
    {
        var index := i;
        var j := i+1;
        while j < a.Length
            invariant 0 <= i < j <= a.Length
            invariant 0 <= index < j
            invariant forall h, k: int ::
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
            invariant forall h, k: int ::
                0 <= h < k < i ==> a[h] <= a[k];
            invariant forall k: int ::
                i <= k < j ==> a[index] <= a[k]
        {
            if a[j] < a[index] {
                index := j;
            }
            j := j + 1;
        }

        var tmp := a[index];
        a[index] := a[i];
        a[i] := tmp;
        assert forall h, k: int :: //error (forall)
            0 <= h < i+1 && i+1 <= k < a.Length ==> a[h] <= a[k];
        assert forall h, k: int :: //error (error forall)
            0 <= h < k < i+1 ==> a[h] <= a[k];
        i := i + 1;
        assert forall h, k: int :: //no more error
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
        assert forall h, k: int :: //no more error
            0 <= h < k < i ==> a[h] <= a[k];
    }
}

Now, note that the assignment with temporary variable:

        var tmp := a[index];
        a[index] := a[i];
        a[i] := tmp;

can actually be simplified in Dafny to:

a[i], a[index] := a[index], a[i];

it makes verification easier for the step below (one step instead of three steps). To move the assertions up this double assignment, we need to ensure we can swap the values a[i] and a[index] in the assertions. For that, we need to explicit what the forall means for these two indices, so that we can swap them.

Since our indices h can be i in the first forall, and k can be i in the second forall, and because we don't know the relative position between index and i, we will need to split the cases. To split the cases, we just insert a if-then-else structure with the conditions, and put back our assertions in them:

method sort(a: array<int>)
    modifies a
    ensures forall h, k: int ::
        0 <= h < k < a.Length ==> a[h] <= a[k];
{
    var i := 0;

    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant forall h, k: int ::
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
        invariant forall h, k: int ::
            0 <= h < k < i ==> a[h] <= a[k];
    {
        var index := i;
        var j := i+1;
        while j < a.Length
            invariant 0 <= i < j <= a.Length
            invariant 0 <= index < j
            invariant forall h, k: int ::
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
            invariant forall h, k: int ::
                0 <= h < k < i ==> a[h] <= a[k];
            invariant forall k: int ::
                i <= k < j ==> a[index] <= a[k]
        {
            if a[j] < a[index] {
                index := j;
            }
            j := j + 1;
        }

        a[i], a[index] := a[index], a[i];
        if i < index {
          assert forall h, k: int ::
            0 <= h < i+1 && i+1 <= k < a.Length ==> a[h] <= a[k];
           assert forall h, k: int ::
            0 <= h < k < i+1 ==> a[h] <= a[k];
        } else if i == index {
          assert forall h, k: int ::
            0 <= h < i+1 && i+1 <= k < a.Length ==> a[h] <= a[k];
          assert forall h, k: int ::
              0 <= h < k < i+1 ==> a[h] <= a[k];
        } else {
          assert forall h, k: int :: //error (forall)
            0 <= h < i+1 && i+1 <= k < a.Length ==> a[h] <= a[k];
          assert forall h, k: int :: //error (forall)
              0 <= h < k < i+1 ==> a[h] <= a[k];
        }
        assert forall h, k: int :: //no more error
            0 <= h < i+1 && i+1 <= k < a.Length ==> a[h] <= a[k];
        assert forall h, k: int :: //no more error
            0 <= h < k < i+1 ==> a[h] <= a[k];
        i := i + 1;
        assert forall h, k: int ::
            0 <= h < i && i <= k < a.Length ==> a[h] <= a[k];
        assert forall h, k: int ::
            0 <= h < k < i ==> a[h] <= a[k];
    }
}

Now, something interesting happens. The assertions are proved if i == index or i < index, but not if index < i. Looking at the inner while loop, it looks like index started at i and is assigned j from time to time, j is increased, and j starts at i+1. Could it be that index <= i in any case?

Let's add the invariant invariant index <= i in the inner loop... Magic, everything verifies now! You can now remove the assertions one by one until you get back to your original code.