class SearchWithBreak {
    /*@ requires arr != null;
      @ ensures arr[\result] == elem || 
      @         (\result == arr.length && 
      @                    !(\exists int k; 0 <= k && k < arr.length; 
      @                     arr[k] == elem));
      @*/
    int linear(int[] arr, int elem) {
	int i;
	/*@
	  @ 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 (i = 0; i < arr.length; i++) {
	    if (arr[i] == elem)
		break;
	}
	return i;
    }
}