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;
}
}
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:
Here is the full method.