Dafny 循环不变量可能不成立

Question

这是一个简单的在数组中分离0和1的问题。我不明白为什么循环不变量不成立。

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;
}

Answer 1

进入你的方法时，前提条件告诉你

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

所以，在那个时候，已知所有的数组元素要么是0，要么是1。然而，由于数组被循环修改，你必须在不变量all中提到你仍然想记住的关于数组内容的事情。

换句话说，要验证循环体保持不变量，将循环体视为从满足不变量的任意状态开始。您可能认为数组元素保持 0 或 1，但您的不变量并没有这么说。这就是为什么您无法证明循环不变量得到维护的原因。

要解决此问题，请添加

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

作为循环不变量。

鲁斯坦

Dafny 循环不变量可能不成立

Dafny Loop Invariant might not Hold

loop-invariant

dafny