/* * Linear and binary search * * 15-122 Principles of Imperative Computation * Frank Pfenning */ bool is_in(int x, int[] A, int lower, int upper) //@requires 0 <= lower && lower <= upper && upper <= \length(A); { for (int i = lower; i < upper; i++) //@loop_invariant lower <= i; if (A[i] == x) return true; return false; } bool is_sorted(int[] A, int lower, int upper) //@requires 0 <= lower && lower <= upper && upper <= \length(A); { for (int i = lower; i < upper-1; i++) /* Careful here: i <= upper-1 is not a loop invariant */ /* Why not? (It *is* preserved by every iteration of the loop.) */ //@loop_invariant lower <= i; { if (!(A[i] <= A[i+1])) return false; } return true; } 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; }