package mysearch;

public class Search {

  /*@ public normal_behavior
    @ requires a != null & a.length >= 0 &&
    @          (\forall int j; 0 <= j && j < a.length; a[j] >= 0);
    @ assignable \nothing;
    @ ensures  (a.length == 0 && \result == -1) ||
    @         (((\forall int j; 0 <= j && j < a.length; a[j] <= \result) &&
    @          (\exists int j; 0 <= j && j < a.length; a[j] == \result)));
    @
    @*/
  public static int searchMax(int[] a) {
    int n = a.length;
    int i = 0;
    int x = -1;
    /*@ loop_invariant 
      @     a != null && a.length >= 0 && n == a.length &&
      @     (\forall int j; 0 <= j && j < n; a[j] >= 0) &&
      @     0 <= i && i <= n &&
      @     ((i == 0 && x == -1 ) ||
      @     (((\forall int j; 0 <= j && j < i; a[j] <= x) &&
      @       (\exists int j; 0 <= j && j < i; a[j] == x))));
      @ decreases (n-i);
      @ assignable x, i;
      @*/
    while (i < n) {
	    if (a[i] > x) {
        x = a[i];
	    }
	    i = i+1;
    }
    return x;
  }
}