Find highest index with value non zero in dafny

Question

In Dafny I want to find the highest index in an int array where the value is != 0 The method requires that such a value exists I tried this but can't figure out how it can't provy any of the ensures clauses. Especially for the clause

ensures 0 <= result

It seems weird, as result can't be assigned when the loop entering conditiong is not fulfilled which is excatly 0 <= i I only could think of more invariants but not any that help.

method HighestNonZeroIndex(arr: array<int>) returns (result: int)
    requires arr.Length >= 1
    requires exists i :: 0 <= i < arr.Length && arr[i] != 0
    ensures 0 <= result 
    ensures result < arr.Length && arr[result] != 0
{
    var i := arr.Length - 1;

    while i >= 0
    invariant -1 <= i < arr.Length
    decreases i
    {
        if arr[i] != 0 {
            result := i;
            return;
    }
    i := i - 1;
    }
}

Answer 1

The problem is that Dafny doesn't realize that because of the requires clause, it is impossible for the while loop to finish normally -- ie, the only way the loop exits is via the return statement.

You need to add more invariants to prove that it is impossible for the loop to exit normally.

I would start with an invariant that says "there exists an index that we haven't visited yet such that the array has a nonzero value in that index".

Answer 2

I added an invariant as described by James, which helped generally but didnt make the method verifiable. I had to take a different approach in making the method theoretically return -1 if there is no not null value. Because of this I had to remove the problematic postcondition clauses anyway. Now this postcondition seems to do the trick:

ensures forall i| 0 <= result < i < arr.Length :: arr[i] == 0

Here is the full method.

method HighestNonZeroIndex(arr: array<int>) returns (result: int)
requires arr.Length > 0
requires exists i :: 0 <= i < arr.Length && arr[i] != 0
ensures 0 <= result < arr.Length ==> arr[result] != 0
ensures forall i| 0 <= result < i < arr.Length :: arr[i] == 0
// the latter ensures clause is not needed
ensures forall i| 0 <= i < arr.Length :: result != -1 ==> arr[i] != 0 
{
   result := -1;
   var i := arr.Length - 1;

   while (i >= 0 && arr[i] == 0)
   invariant (0 <= i < arr.Length -1 )  ==> arr[i+1] == 0
   invariant result == -1 ==> forall x :: 0 <= i < x < arr.Length ==> arr[x] == 0
   invariant exists j :: 0 <= j <= i && arr[j] != 0
   invariant result != -1 ==> arr[result] != 0
   decreases i
   {
       if(arr[i] != 0)
       {
           result := i;
           return;    
       }
       i := i - 1;
   }
}