Dafny, Dutch Flag, loop invariant might not be maintained by the loop

Question

in the program below I am creating something like Dutch national flag problem and following the same logic which is also provided here the program sorts array of 0s,1s and 2s in the manner all 1s in the beginning 0s in the middle and 2s at the end. [1,1,1,0,0,2,2,2]. but at the loop invariants, I get the error This loop invariant might not be maintained by the loop.

initially, i and j are at index 0, and k at last index. the logic is that j moves up if it sees 2, swap with k and k reduces if sees 0 just j moves up, and if sees 1 swap with i and both i and j increase.

the code is also here in rise4fun

        method sort(input: array?<int>)
        modifies input
        requires input !=null;
        requires input.Length>0;
        requires forall x::0<=x<input.Length ==> input[x]==0||input[x]==1||input[x]==2;
        ensures sorted(input);
        {
            var k: int := input.Length;
            var i, j: int := 0 , 0;
            while(j != k )
            invariant 0<=i<=j<=k<=input.Length;
/* the following invariants might not be maintained by the loop.*/
            invariant forall x:: 0<=x<i ==> input[x]==1;
            invariant forall x:: i<=x<j ==> input[x]==0;
            invariant forall x:: k<=x<input.Length ==> input[x]==2;
            invariant forall x:: j<=x<k ==> input[x]==0||input[x]==1||input[x]==2;
            decreases if j <= k then k - j else j - k
            {
                if(input[j] == 2){
                    swap(input, j, k-1);
                    k := k - 1;
                } else if(input[j] == 0){
                    j := j + 1;
                } else {
                    swap(input, i, j);
                    i:= i + 1;
                    j := j + 1;
                }
               }
            }

and here are swap method and sorted predicate

    predicate sorted(input:array?<int>)
    requires input!=null;
    requires input.Length>0;
    reads input;
    {
        forall i,j::0<=i<j<input.Length ==> input[i]==1 || input[i]==input[j] || input[j]==2
    }

    method swap(input: array?<int>, n:int, m:int)
    modifies input;
    requires input!=null;
    requires input.Length>0;
    requires 0<=n<input.Length && 0<=m<input.Length
    {
        var tmp : int := input[n];
        input[n] := input[m];
        input[m] := tmp;
    }

Answer 1

The problem is that swap has no postcondition. The default postcondition is true, so the specification of swap says that it changes the array in any arbitrary way.

When the verifier sees a call to swap in the body of method sort, it only pays attention to swap's specification --- not it's body. Thus, after the call to swap, the array could have any values in it at all, at least as far as the verifier can tell. So it is hardly surpising that any invariant relating to the contents of the array can not be proved.

The following specification for swap should work:

method swap(input: array?<int>, n:int, m:int)
    modifies input;
    requires input!=null;
    requires input.Length>0;
    requires 0<=n<input.Length && 0<=m<input.Length
    ensures n < m ==> input[..] == old( input[0..n] + [input[m]] + input[n+1..m] + [input[n]] + input[m+1..] ) ;
    ensures n==m ==> input[..] == old(input[..])
    ensures n > m ==> input[..] == old( input[0..m] + [input[n]] + input[m+1..n] + [input[m]] + input[n+1..] ) ;

So should this

method swap(input: array?<int>, n:int, m:int)
    modifies input;
    requires input!=null;
    requires input.Length>0;
    requires 0<=n<input.Length && 0<=m<input.Length
    ensures input[n] == old( input[m] ) ;
    ensures input[m] == old( input[n] ) ;
    ensures forall i | 0 <= i < input.Length && i != n && i != m :: input[i] == old(input[i])