Dafny中循环变量能否设任意大上界？线性搜索终止性验证问题

不是完全无法表达，只是需要给循环提供明确的终止度量，让Dafny能证明循环一定会停止。

你写的无界循环代码过不了验证，是因为Dafny默认要求循环的终止性必须可证：虽然你的前置条件保证了存在首个满足f(n)=True的自然数，但Dafny没法自动把这个存在性和循环的终止关联起来，需要你明确给出一个严格递减的良序度量。

修正后的可验证代码 #

method linear_search(f: nat -> bool) returns (x: nat)
    requires exists n : nat :: f(n)
    ensures f(x) && forall i : nat :: i < x ==> !f(i)
{
    x := 0;
    // 取出前置条件中存在的最小满足f(n)的自然数k
    var k : nat := min n : nat where f(n);
    while !f(x)
        decreases k - x  // 终止度量：每次循环后k-x严格递减，且始终非负
        invariant forall i : nat :: i < x ==> !f(i)  // 确保x之前的数都不满足f
    {
        x := x + 1;
    }
}

关键说明 #

1. 终止度量的选择：
   用k - x作为decreases子句的内容，其中k是第一个满足f(n)=True的自然数。因为循环条件是!f(x)，结合k的最小性，可知x始终小于k，所以k - x是自然数（非负）；每次循环x加1，这个值会严格递减，符合Dafny对终止性的要求（良序集上的严格递减序列必然有限）。
2. 循环不变式的作用：
   不变式forall i : nat :: i < x ==> !f(i)保证了在循环过程中，x之前的所有自然数都不满足f，配合循环结束时f(x)=True的条件，就能证明返回的x是首个满足条件的数。
3. 隐式度量的写法：
   也可以不用显式声明k，直接把decreases子句写成(min n : nat where f(n)) - x，效果一样，只是显式声明k会让代码可读性更好。

你的有界搜索能过验证，本质是用max_bound - x作为终止度量，而无界场景只是把“已知的max_bound”换成了“前置条件中存在的最小k”，核心逻辑是一致的。

内容的提问来源于stack exchange，提问作者Germán Ferrero