(Dafny) Searching in an array - loop variant bounded by zero?

Question

Consider the following Dafny code that tries to find an element e inside an array a :

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

The verification works fine but there is something that I am not sure to understand : if I am not mistaken, the variant of a loop, if it is an integer, must be bounded by zero. However u-i goes below zero when i = u+1 at the last iteration. Why doesn't Dafny complain about u-i not being bounded by zero?

Answer 1

You're right that the variant (which Dafny calls the decreases clause) must be bounded below. But Dafny allows any lower bound, not just 0.

In your case, the loop invariant i <= u + 1 implies that -1 <= u - i, so the decreases clause is bounded below.

For more information see section 21.10.0.1 of the Dafny Reference Manual.