Dafny 中的循环变量可以有一个任意大的上限吗？

Question

我正在尝试在 Dafny 中编写“线性搜索”方法。该方法采用一个函数

f

将自然数映射到布尔值，并且已知存在第一个数字

n

，其中

f(n) == True

。然后该方法确保

n

是返回值。
当然，根据这个规范，

n

可以是任意大的，并且只有在假设有任意大的可用能量的情况下，才能确保程序能够找到

n

。

这是 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;
    while !f(x)
    {
        x := x + 1;
    }
}

验证器失败并显示：“无法证明终止；尝试为循环提供减少子句”

另一种有界线性搜索已经过验证，没有任何问题。

method bounded_linear_search(f: nat -> bool, max_bound: nat) returns (x: nat)
    requires exists n : nat :: n <= max_bound && f(n)
    ensures f(x) && forall i : nat :: i < x ==> !f(i)
{
    x := 0;
    while !f(x) && x <= max_bound
        decreases max_bound - x
        invariant forall i : nat :: i < x ==> !f(i)
    {
        x := x + 1;
    }
}

Answer 1

您可以通过使用幽灵变量以及向循环添加必要的不变量来验证原始版本。幽灵变量是一个可以用来保存附加信息以进行验证的变量，但不是可编译代码的一部分。

module SO6 {
    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)
    {
        ghost var n: nat :| f(n);
        x := 0;
        while !f(x)
            invariant x <= n
            invariant forall i : nat :: i < x ==> !f(i)
            decreases n - x
        {
            x := x + 1;
        }
        assert f(x);
    }

}