Iterative algorithm and functional code (Dafny)

I have this simple algorithm + functions:

method DifferenceMinMax(a: array<int>) returns (diff: int)
    requires a.Length > 0
    ensures diff == (Max(a[..]) - Min(a[..]))
{
    var minVal := a[0];
    var maxVal := a[0];

    for i := 1 to a.Length
        invariant 1 <= i <= a.Length
        invariant minVal <= maxVal
        invariant forall k :: 0 <= k < i ==> minVal <= a[k] && a[k] <= maxVal
    {
        if a[i] < minVal {
            minVal := a[i];
        } else if a[i] > maxVal {
            maxVal := a[i];
        }
    }

    diff := maxVal - minVal;
}

function Min(a: seq<int>) : int
    requires |a| > 0
{
    if |a| == 1 then a[0]
    else if a[0] <= Min(a[1..]) then a[0] else Min(a[1..])
}

function Max(a: seq<int>) : int
    requires |a| > 0
{
    if |a| == 1 then a[0]
    else if a[0] >= Max(a[1..]) then a[0] else Max(a[1..])
}

This doesn't verify.

I know I can rewrite the method like this:

method DifferenceMinMax(a: array<int>) returns (diff: int)
    requires a.Length > 0
    ensures diff == (Max(a[..]) - Min(a[..]))
{
    var minVal := Min(a[..]);
    var maxVal := Max(a[..]);

    diff := maxVal - minVal;
}

This verifies. But this traverses the array twice, while the first iterative solution does it only once. Assume I really want the first iterative algorithm. How do I define Max and Min so that the returned diff is really the difference between the max and the min?

I already tried this, which I was hoping to use in the loop invariant somehow, but it doesn't verify:

function Min(a: seq<int>) : (m: int)
    requires |a| > 0
    ensures forall n :: n in a ==> m in a && m <= n
{
    if |a| == 1 then a[0]
    else if a[0] <= Min(a[1..]) then a[0] else Min(a[1..])
}

Do I need to get rid of the functions entirely?
Thanks.

Great question.

Here is some advice on how to solve such an issue, and below is the solution

Advice

• In your loop, you effectively compute min(min(min(a[0], a[1]), a[2]), a[3]). Looking at that, it is best practice to ensure your specification of the minimum matches this computation. Your current spec computes min(a[0], min(a[1], min(a[2]....))) so you'll have a hard time (meaning, needing a lemma) to prove that the two are the same, or postconditions (I haven't tried that)
• If a for loop is failing to verify (i.e. some invariants), it's better to convert it temporarily to a while loop and explicit the assignments of the loop variable
• Write the invariant as an assertion that should hold at the end of the for loop
• Apply the weakest precondition calculus to see what should hold at the beginning
• In your min and max function, you compute the same function twice, you can assign it to a variable
• You need to have an invariant that produces something about MinVal(a) and MaxVal(a) at the end.

That advice given, here is the solution.

*** Solution ***

method DifferenceMinMax(a: array<int>) returns (diff: int)
    requires a.Length > 0
    ensures diff == (Max(a[..]) - Min(a[..]))
{
    var minVal := a[0];
    var maxVal := a[0];
    for i := 1 to a.Length
        invariant 1 <= i <= a.Length
        invariant minVal <= maxVal
        invariant forall k :: 0 <= k < i ==> minVal <= a[k] && a[k] <= maxVal
        invariant minVal == Min(a[..i])
        invariant maxVal == Max(a[..i])
    {
        if a[i] < minVal {
            minVal := a[i];
        } else if a[i] > maxVal {
            maxVal := a[i];
        }
        assert a[..i+1][..i] == a[..i];
    }
    assert a[..a.Length] == a[..];
    diff := maxVal - minVal;
}

function Min(a: seq<int>) : (m: int)
    requires |a| > 0
{
    if |a| == 1 then a[0]
    else
      var minPrefix := Min(a[..|a|-1]);
      if a[|a|-1] <= minPrefix then a[|a|-1] else minPrefix
}

function Max(a: seq<int>) : (m: int)
    requires |a| > 0
{
    if |a| == 1 then a[0]
    else
      var maxPrefix := Max(a[..|a|-1]);
      if a[|a|-1] >= maxPrefix then a[|a|-1] else maxPrefix
}