时间戳

首页 > 解决方案 > Dafny 循环不变量可能不成立

dafny - Dafny 循环不变量可能不成立

问题描述

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

标签： dafnyloop-invariant

解决方案

在进入您的方法时，前提条件会告诉您

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

所以，在那个时候，已知所有的数组元素都是0or 或1。但是，由于数组是由循环修改的，因此您必须在不变量中提及您仍想记住的有关数组内容的所有内容。

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

要解决此问题，请添加

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

作为循环不变量。

鲁斯坦

推荐阅读