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+1Dafny がu-iゼロに制限されていないことについて文句を言わないのはなぜですか?