Dafny方法BadNbr验证失败：断言v==0不成立，求后置条件优化方案

我实现了Dafny方法BadNbr，用于返回第一个“坏邻居”的最小索引，若不存在则返回-1。规则定义：若相邻元素对的和为负数，则右侧元素被称为“坏邻居”（数组为循环结构，最后一个元素的邻居是第一个元素）。例如：

• 数组[0,-1]、[-1,0]、[0,0,-1]的负和对为循环相邻，右侧元素索引0是坏邻居；
• 数组[-1,0,1]的负和对在索引0、1处，右侧元素索引1是坏邻居。

当前在验证方法TestBadNbr中，断言v == 0出现“断言可能不成立”的错误，需要强化BadNbr的后置条件来解决该问题。

原代码 #

method BadNbr(a: array<int>) returns (bn: int)
    ensures bn == -1 || (0 <= bn < a.Length && a[(bn - 1 + a.Length) % a.Length] + a[bn] < 0)
{
    bn := -1;

    if a.Length < 2 {
        return bn; // No neighbors to check
    }

    // Loops through the array to find the first bad neighbor
    var i := 0;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant bn == -1 || (0 <= bn < a.Length && a[(bn - 1 + a.Length) % a.Length] + a[bn] < 0)
    {
        var leftNeighbor := (i - 1 + a.Length) % a.Length;
        if a[leftNeighbor] + a[i] < 0 {
            bn := i;
            return;
        }
        i := i + 1;
    }
}

// Validator method
method TestBadNbr()
{
    var arr := new int[2];
    arr[0], arr[1] := 0, -1;
    var v: int := BadNbr(arr);
    assert v == 0;

    // Further testing todo
}

问题分析 #

当前的后置条件仅保证返回值要么是-1，要么是一个合法的坏邻居，但没有明确返回的坏邻居是索引最小的第一个符合条件的元素，也没有说明当返回-1时所有元素都不是坏邻居。验证器无法从现有条件推导出测试用例中必然返回0，因此断言失败。

修改后的代码 #

method BadNbr(a: array<int>) returns (bn: int)
    ensures bn == -1 || (0 <= bn < a.Length && a[(bn - 1 + a.Length) % a.Length] + a[bn] < 0)
    // 新增：保证bn是第一个（最小索引）的坏邻居，前面的元素都不是
    ensures bn != -1 ==> (forall k: int :: 0 <= k < bn ==> a[(k - 1 + a.Length) % a.Length] + a[k] >= 0)
    // 新增：保证当返回-1时，所有元素都不是坏邻居
    ensures bn == -1 ==> (forall k: int :: 0 <= k < a.Length ==> a[(k - 1 + a.Length) % a.Length] + a[k] >= 0)
{
    bn := -1;

    if a.Length < 2 {
        return bn; // No neighbors to check
    }

    var i := 0;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant bn == -1 || (0 <= bn < a.Length && a[(bn - 1 + a.Length) % a.Length] + a[bn] < 0)
        // 新增循环不变式：当bn未找到时，前i个元素都不是坏邻居
        invariant bn == -1 ==> (forall k: int :: 0 <= k < i ==> a[(k - 1 + a.Length) % a.Length] + a[k] >= 0)
        // 新增循环不变式：当bn已找到时，它是第一个符合条件的，前面的都不是
        invariant bn != -1 ==> (bn < i && forall k: int :: 0 <= k < bn ==> a[(k - 1 + a.Length) % a.Length] + a[k] >= 0)
    {
        var leftNeighbor := (i - 1 + a.Length) % a.Length;
        if a[leftNeighbor] + a[i] < 0 {
            bn := i;
            return;
        }
        i := i + 1;
    }
}

// Validator method
method TestBadNbr()
{
    var arr := new int[2];
    arr[0], arr[1] := 0, -1;
    var v: int := BadNbr(arr);
    assert v == 0;

    // Further testing todo
}

关键修改说明 #

1. 后置条件强化：
   • 当bn != -1时，通过forall断言保证所有索引小于bn的元素都不是坏邻居，明确bn是第一个符合条件的元素；
   • 当bn == -1时，保证数组中不存在任何坏邻居，补充了完整性条件。
2. 循环不变式强化：
   • 在循环过程中维护“未找到坏邻居时，已遍历的元素都不是坏邻居”的性质；
   • 若已找到坏邻居，维护“该邻居是第一个符合条件的，且前面的元素都不是”的性质，确保循环过程中不变式始终成立，帮助验证器推导最终结果。

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