class Search {
    /*@ requires arr != null;
      @ ensures \result == (\exists int k; 0 <= k && k < arr.length; 
      @                     arr[k] == elem);
      @*/
    boolean linear(int[] arr, int elem) {
	/*@
	  @ loop_invariant !(\exists int k; 0 <= k && k < i; arr[k] == elem);
	  @ loop_invariant 0 <= i && i <= arr.length;
	  @ modifies i;
	  @ decreases arr.length - i;
	  @*/
	for (int i = 0; i < arr.length; i++) {
	    if (arr[i] == elem)
		return true;
	}
	return false;
    }


    /*@ requires arr != null;
      @ requires (\forall int j,k; 0 <= j && j <= k && k < arr.length;
      @                      arr[j] <= arr[k]);  // array is sorted
      @ ensures \result == (\exists int k; 0 <= k && k < arr.length; 
      @                                arr[k] == elem);
      @*/
    boolean binary(int[] arr, int elem) {
	int lower = 0, upper = arr.length - 1;
	/*@
	  @ loop_invariant lower >= 0 && upper < arr.length;
	  @ loop_invariant !(\exists int k; 0 <= k && k < arr.length; 
	  @                      (k < lower || k > upper) && arr[k] == elem);
	  @ modifies lower, upper;
	  @ decreases upper - lower + 1;
	  @*/
	while (lower <= upper) {
	    int mid = (lower + upper) / 2;
	    assert lower <= mid && mid <= upper;
	    if (arr[mid] == elem) {
		return true;
	    } else if (arr[mid] > elem) {
		upper = mid-1;
	    } else {
		lower = mid+1;
	    }
	}
	return false;
    }
}