int search(int x, int[] A, int n) //@requires 0 <= n && n <= \length(A); //@requires is_sorted(A, 0, n); /*@ensures (-1 == \result && !is_in(x, A, 0, n)) || ((0 <= \result && \result < n) && A[\result] == x); @*/ { for (int i = 0; i < n; i++) //@loop_invariant 0 <= i && i <= n; //@loop_invariant i == 0 || x > A[i-1]; { if (A[i] == x) return i; else if (x < A[i]) return -1; //@assert A[i] < x; } //@assert n == 0 || x > A[n-1]; return -1; }