CODEWITHSUNDEEP
dafnyloop-invariant
tn2000
tn2000

Reputation: 23

Dafny Loop Invariant might not Hold

This is a simple segregating 0s and 1s in the array problem. I can't fathom why the loop invariant does not hold.

method rearrange(arr: array<int>, N: int) returns (front: int)
    requires N == arr.Length
    requires forall i :: 0 <= i < arr.Length ==> arr[i] == 0 || arr[i] == 1
    modifies arr
    ensures 0 <= front <= arr.Length
    ensures forall i :: 0 <= i <= front - 1 ==> arr[i] == 0
    ensures forall j :: front <= j <= N - 1 ==> arr[j] == 1
{
    front := 0;
    var back := N;
    while(front < back)
        invariant 0 <= front <= back <= N
        invariant forall i :: 0 <= i <= front - 1 ==> arr[i] == 0
        // The first one does not hold, the second one holds though
        invariant forall j :: back <= j < N ==> arr[j] == 1
    {
        if(arr[front] == 1){
            arr[front], arr[back - 1] := arr[back - 1], arr[front];
            back := back - 1;
        }else{
            front := front + 1;
        }
    }
    return front;
}

Upvotes: 0

Views: 817

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

On entry to your method, the precondition tells you

forall i :: 0 <= i < arr.Length ==> arr[i] == 0 || arr[i] == 1

So, at that time, it is known that all array elements are either 0 or 1. However, since the array is modified by the loop, you must mention in invariants all the things you still want to remember about the contents of the array.

In different words, to verify that the loop body maintains the invariant, think of the loop body as starting in an arbitrary state satisfying the invariant. You may have in your mind that array elements remain 0 or 1, but your invariant does not say that. This is why you're unable to prove that the loop invariant is maintained.

To fix the problem, add

forall i :: 0 <= i < arr.Length ==> arr[i] == 0 || arr[i] == 1

as a loop invariant.

Rustan

Upvotes: 1

Related Questions