(Dafny) 在数组中搜索 - 以零为界的循环变体？

Question

考虑以下 Dafny 代码，它试图在数组 a[=21= 中找到元素 e ] :

method findE(a:array<int>, e:int, l:int, u:int) returns (result:bool)
    requires a != null
    requires 0 <= l <= u < a.Length
    ensures result <==> exists k | l <= k <= u :: a[k] == e
{   
    var i := l;

    while i <= u 
        invariant l <= i <= u+1
        invariant !(exists k | l <= k < i :: a[k] == e)
        decreases u-i
    {
        if a[i] == e {
            result :=   true;
            return;
        }   
        i := i+1;
    }
    result :=   false;
}

验证工作正常但有些事情我不确定是否理解：如果我没记错的话，循环的变体，如果它是一个整数，必须以零为界。然而，当 i = u+1 在最后一次迭代时，u-i 低于零。为什么 Dafny 不抱怨 u-i 没有被零限制？

Answer 1

你说得对，变体（Dafny 称之为减少子句）必须在下方有界。但是 Dafny 允许任何下限，而不仅仅是 0。

在你的例子中，循环不变量 i <= u + 1 意味着 -1 <= u - i，因此 decreases 子句在下面有界。

有关详细信息，请参阅 Dafny Reference Manual 的第 21.10.0.1 节。