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

Question

考虑以下尝试在数组a中查找元素e的Dafny代码：

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;
}

验证工作正常，但有些东西我不确定：如果我没记错的话，循环的变体（如果它是整数）必须以零为界。然而，在最后一次迭代u-i时低于零。i = u+1为什么 Dafny 不抱怨u-i不受零约束？

Answer 1

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

在您的情况下，循环不变量i <= u + 1意味着-1 <= u - i，因此减少子句在下面有界。

有关详细信息，请参阅Dafny 参考手册的第 21.10.0.1 节。