/* * Linear and binary search * * 15-122 Principles of Imperative Computation * Frank Pfenning, Rob Simmons */ 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; } /* gt_seg(x, A, lower, upper) * iff x > A[lower..upper) * iff x > A[i] for all lower <= i < upper */ bool gt_seg(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 && i <= upper; { if (!(x > A[i])) 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++) // 0 <= i is necessary for safety in the loop, and i <= n is // neccessary both as a safety precondition for the other loop // invariants and to help the other loop invariants imply the // postcondition by ensuring that i == n after the loop // terminates. //@loop_invariant 0 <= i && i <= n; // All three of these loop invariants are preserved and imply the // postcondition. Only the !is_in loop invariant will ensure // correctness of searching through an *unsorted* array, however. //@loop_invariant i == 0 || x > A[i-1]; //@loop_invariant gt_seg(x, A, 0, i); //@loop_invariant !is_in(x, A, 0, i); { if (A[i] == x) return i; else if (A[i] > x) return -1; //@assert A[i] < x; } //@assert n == 0 || x > A[n-1]; //@assert gt_seg(x, A, 0, n); //@assert !is_in(x, A, 0, n); return -1; }