A Dafny solution to the Sum and Max verification benchmark. I added some additional specification to verify that the result `max`

is really the maximum and the `sum`

is really the sum.

method SumMax(a: array<int>) returns (sum:int, max:int) requires a != null; requires a.Length >= 0; requires forall i :: 0 <= i < a.Length ==> a[i] >= 0; ensures sum <= a.Length*max; ensures forall i :: 0 <= i < a.Length ==> a[i] <= max; ensures a.Length == 0 || (exists i :: 0 <= i < a.Length && a[i] == max); ensures sum == Sum(a); { max := 0; sum := 0; var idx:int := 0; while idx<a.Length invariant idx <= a.Length; invariant forall i :: 0 <= i < idx ==> a[i] <= max; invariant (idx==0 && max==0) || exists i :: 0 <= i < idx && a[i] == max; invariant sum <= idx*max; invariant sum == Sum'(a, 0, idx); { if (max < a[idx]) { max := a[idx]; } sum := sum + a[idx]; idx := idx + 1; } } function Sum(a: array<int>) : int reads a; requires a != null; { Sum'(a, 0, a.Length) } function Sum'(a: array<int>, i:int, j:int) : int reads a; requires a != null; requires 0 <= i <= j <= a.Length; { if j == i then 0 else Sum'(a, i, j-1) + a[j-1] } lemma SumOfIntervalOneIsElement(a: array<int>, i:int) requires a != null; requires 0 <= i < a.Length; ensures a.Length > 0; ensures Sum'(a, i, i+1) == a[i]; { } lemma SumOfIntervalIsSumOfSubIntervals (a: array<int>, i:int, j:int, k:int) requires a != null; requires 0 <= i <= j <= k <= a.Length; ensures Sum'(a, i, j) + Sum'(a, j, k) == Sum'(a, i, k); { } |