OpenJML Examples: Sum Max

Given an array of integers, prove that the running max is at least n times the running sum, where n is the number of elements so far.

public class SumMax {


  //@ requires a.length > 0;
  void m(int[] a) {
    int sum = 0;
    int max = a[0];

    //@ loop_invariant 0 <= i <= a.length;
    //@ loop_invariant sum <= \count * max;  // Assertion to be proved
    for (int i=0; i<a.length; i++) {
      //@ assume Integer.MIN_VALUE <= sum + a[i] <= Integer.MAX_VALUE; // Just assume we never overflow
      sum += a[i];
      if (max < a[i]) max = a[i];
    }
  }

}