我正在尝试用 Dafny 编写一个“线性搜索”方法。该方法采用将f自然数映射到布尔值的函数，并且已知存在第一个数字，n使得f(n) == True。然后该方法确保 n是返回值。根据此规范，
自然n可以是任意大的，并且只有在假设可用能量任意大的情况下，才能确保程序能够找到n。
这难道不是达芙妮无法表达的吗？
这是我尝试过的
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;
}
}