Find the maximum element of an array by searching in from the ends
public class MaxByElimination {
//@ requires a != null && a.length > 0;
//@ ensures 0 <= \result < a.length;
//@ ensures (\forall int i; 0 <= i < a.length; a[i] <= a[\result]);
public static int max(int[] a) {
int x = 0;
int y = a.length-1;
//@ loop_invariant 0 <= x <= y < a.length;
// So far either a[y] is the largest or a[x] is the largest of everything beyond x and beyond y (not including a[x] and a[y])
/*@ loop_invariant ((\forall int i; 0<=i && i<x; a[i] <= a[y]) && (\forall int i; y < i && i < a.length; a[i] <= a[y]))
|| ((\forall int i; 0<=i && i<x; a[i] <= a[x]) && (\forall int i; y < i && i < a.length; a[i] <= a[x]));
*/
//@ decreases y-x;
while (x != y) {
if (a[x] <= a[y]) x++;
else y--;
}
return x;
}
}