（Dafny）在數組中搜索 - 以零爲界的循環變體？

Question

考慮以下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稱之爲decrease子句）必須在下面有界。但Dafny允許任何下限，而不僅僅是0.

在你的情況下，循環不變量i <= u + 1意味着-1 <= u - i，所以reduce子句在下面有界。

欲瞭解更多信息，請參閱Dafny Reference Manual的21.10.0.1節。