Index out of range in "var max: int := a[0];"

Question

Here is my Dafny code that finds the index of an input array such that the value in the array at that index is the maximal. However, Dafny indicates that there is an index out of range problem on line 8 (var max: int := a[0];). This is highly confusing as it seems trivially correct. Can anyone offer insights to this problem?

method FindMax(a: array<int>) returns (index: int)
    ensures 0 <= index && index < a.Length
    ensures forall i:: 0 <= i && i < a.Length && i != index ==> a[i] <= a[index]
{
    // Can you write code that satisfies the postcondition?
    // Hint: you can do it with one statement.
    var i: nat := 0;
    var max: int := a[0]; // index out of range ???
    var max_idx: int := i;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant 0 <= max_idx <= a.Length
    {
        if a[i] > max 
        {
            max_idx := i;
            max := a[i];
        }
        i := i + 1;
    }
    return max_idx;
}

I ran this code in VS Code with Dafny extension installed.

Answer 1

Your algorithm is underspecified. You must account for how all variables evolve in your algorithm to prove it works. Also, any property that you want to maintain in your loop must also be specified.

method FindMax(a: array<int>) returns (index: int)
    requires a.Length > 0
    ensures 0 <= index && index < a.Length
    ensures forall i:: 0 <= i && i < a.Length && i != index ==> a[i] <= a[index]
{
    var i: nat := 0;
    var max: int := a[0];
    var max_idx: int := i;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant 0 <= max_idx < a.Length
        invariant max == a[max_idx]
        invariant forall k :: 0 <= k < i ==> a[k] <= a[max_idx]
    {
        if a[i] > max 
        {
            max_idx := i;
            max := a[i];
        }
        i := i + 1;
    }
    return max_idx;
}

You can simplify it a little as well.

method FindMax(a: array<int>) returns (index: int)
    requires a.Length > 0
    ensures 0 <= index < a.Length
    ensures forall i:: 0 <= i < a.Length && i != index ==> a[i] <= a[index]
{
    var i: nat := 0;
    var max_idx: int := i;
    while i < a.Length
        invariant 0 <= i <= a.Length
        invariant 0 <= max_idx < a.Length
        invariant forall k :: 0 <= k < i ==> a[k] <= a[max_idx]
    {
        if a[i] > a[max_idx]
        {
            max_idx := i;
        }
        i := i + 1;
    }
    return max_idx;
}