Dafny数组条件修改问题：循环不变量无法维持错误求助

问题背景 #

形式化需求：给定数组arr和整数k，当且仅当arr[i] > k时，将arr[i]修改为-1。

以下是尝试实现的Dafny代码：

method replace(arr: array?<int>, k: int)
    modifies arr
    
    // precondition: non-null array
    requires arr != null && arr.Length > 0;
    requires forall i :: 0 <= i < arr.Length ==> arr[i] > 0

    // postcondition
    ensures forall i :: 0 <= i < arr.Length ==> (old(arr[i]) > k ==> arr[i] == -1) && (old(arr[i]) <= k ==> arr[i] == old(arr[i]))
{
    var i := 0;
    while i < arr.Length
        // variant
        decreases arr.Length - i
        
        // invariants
        invariant 0 <= i <= arr.Length

        // ERROR HERE!
        invariant forall j :: 0 <= j < i ==> (old(arr[j]) > k ==> arr[j] == -1) && (old(arr[j]) <= k ==> arr[j] == old(arr[j]))
    {
       if (arr[i] > k)
       {
         arr[i] := -1;
       }
        
       i := i + 1;
    }
}

Dafny报错信息：

ex2.dfy(140,12): Error: This loop invariant might not be maintained by the loop.
ex2.dfy(140,12): Related message: loop invariant violation

问题原因 #

报错核心是Dafny无法自动推断：处理索引i时，当前arr[i]仍等于方法初始状态的old(arr[i])。现有不变量仅描述了已处理元素（j < i）的状态，但未明确未处理元素（j >= i）仍保持初始值，导致验证器无法确认循环体对arr[i]的修改符合不变量要求。

修复方案 #

添加一个新的循环不变量，明确未处理元素尚未被修改：

invariant forall j :: i <= j < arr.Length ==> arr[j] == old(arr[j])

完整修复后的代码：

method replace(arr: array?<int>, k: int)
    modifies arr
    
    // precondition: non-null array
    requires arr != null && arr.Length > 0;
    requires forall i :: 0 <= i < arr.Length ==> arr[i] > 0

    // postcondition
    ensures forall i :: 0 <= i < arr.Length ==> (old(arr[i]) > k ==> arr[i] == -1) && (old(arr[i]) <= k ==> arr[i] == old(arr[i]))
{
    var i := 0;
    while i < arr.Length
        // variant
        decreases arr.Length - i
        
        // invariants
        invariant 0 <= i <= arr.Length
        invariant forall j :: 0 <= j < i ==> (old(arr[j]) > k ==> arr[j] == -1) && (old(arr[j]) <= k ==> arr[j] == old(arr[j]))
        invariant forall j :: i <= j < arr.Length ==> arr[j] == old(arr[j])
    {
       if (arr[i] > k)
       {
         arr[i] := -1;
       }
        
       i := i + 1;
    }
}

验证逻辑说明 #

1. 初始化阶段：i=0，未处理元素覆盖整个数组，arr[j] == old(arr[j])显然成立；已处理元素为空，第一个量化不变量 vacuously true（空范围的全称断言自动成立）。
2. 循环体执行：
   • 进入循环时，未处理元素从i开始，因此arr[i]等于初始值old(arr[i])，此时判断arr[i] > k等价于判断old(arr[i]) > k。
   • 修改arr[i]后，i递增为i+1，新的未处理元素从i+1开始，仍保持初始值；已处理元素新增i位置，完全符合第一个不变量的要求。
3. 循环结束：i=arr.Length，第一个不变量覆盖整个数组，直接满足后置条件。

内容的提问来源于stack exchange，提问作者MooDoesCow