Dafny 循环不变量可能不成立

【问题标题】：Dafny Loop Invariant might not HoldDafny 循环不变量可能不成立
【发布时间】：2020-02-19 02:35:12
【问题描述】：

这是一个简单的在数组中分离 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;
}

【问题讨论】：

标签： dafny loop-invariant

【解决方案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

作为循环不变量。

鲁斯坦

【讨论】：