/* Utility functions for working with arrays of integers * Mostly specification functions, but swap is effectful * * 15-122 Principles of Imperative Computation */ /*** Interface ***/ /* is_in: x in A[lower,upper) */ bool is_in(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ ; /* is_sorted: A[lower,upper) SORTED */ bool is_sorted(int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ ; /* swap(A, i, j) has the effect of switching A[i] and A[j] */ void swap(int[] A, int i, int j) /*@ requires 0 <= i && i < \length(A) && 0 <= j && j < \length(A); @*/ ; /* gt_seg: x > A[lower,upper) */ bool gt_seg(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ ; /* ge_seg: x >= A[lower,upper) */ bool ge_seg(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ ; /* lt_seg: x < A[lower,upper) */ bool lt_seg(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ ; /* le_seg: x <= A[lower,upper) */ bool le_seg(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ ; /* gt_segs: A[lower1,upper1) > B[lower2,upper2) */ bool gt_segs(int[] A, int lower1, int upper1, int[] B, int lower2, int upper2) /*@requires 0 <= lower1 && lower1 <= upper1 && upper1 <= \length(A); @*/ /*@requires 0 <= lower2 && lower2 <= upper2 && upper2 <= \length(B); @*/ ; /* ge_segs: A[lower1,upper1) >= B[lower2,upper2) */ bool ge_segs(int[] A, int lower1, int upper1, int[] B, int lower2, int upper2) /*@requires 0 <= lower1 && lower1 <= upper1 && upper1 <= \length(A); @*/ /*@requires 0 <= lower2 && lower2 <= upper2 && upper2 <= \length(B); @*/ ; /* lt_segs: A[lower1,upper1) < B[lower2,upper2) */ bool lt_segs(int[] A, int lower1, int upper1, int[] B, int lower2, int upper2) /*@requires 0 <= lower1 && lower1 <= upper1 && upper1 <= \length(A); @*/ /*@requires 0 <= lower2 && lower2 <= upper2 && upper2 <= \length(B); @*/ ; /* le_segs: A[lower1,upper1) <= B[lower2,upper2) */ bool le_segs(int[] A, int lower1, int upper1, int[] B, int lower2, int upper2) /*@requires 0 <= lower1 && lower1 <= upper1 && upper1 <= \length(A); @*/ /*@requires 0 <= lower2 && lower2 <= upper2 && upper2 <= \length(B); @*/ ; /*** Implementation ***/ bool is_in(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ { if (lower == upper) return false; return A[lower] == x || is_in(x,A,lower+1,upper); } void swap(int[] A, int i, int j) //@requires 0 <= i && i < \length(A); //@requires 0 <= j && j < \length(A); { int tmp = A[i]; A[i] = A[j]; A[j] = tmp; } bool gt_seg(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ { if (lower == upper) return true; return x > A[lower] && gt_seg(x, A, lower+1, upper); } bool ge_seg(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ { if (lower == upper) return true; return x >= A[lower] && ge_seg(x, A, lower+1, upper); } bool lt_seg(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ { if (lower == upper) return true; return x < A[lower] && lt_seg(x, A, lower+1, upper); } bool le_seg(int x, int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ { if (lower == upper) return true; return x <= A[lower] && le_seg(x, A, lower+1, upper); } bool is_sorted(int[] A, int lower, int upper) /*@requires 0 <= lower && lower <= upper && upper <= \length(A); @*/ { if (lower == upper) return true; return le_seg(A[lower], A, lower+1, upper) && is_sorted(A, lower+1, upper); } bool gt_segs(int[] A, int lower1, int upper1, int[] B, int lower2, int upper2) //@requires 0 <= lower1 && lower1 <= upper1 && upper1 <= \length(A); //@requires 0 <= lower2 && lower2 <= upper2 && upper2 <= \length(B); { if (lower1 == upper1) return true; return gt_seg(A[lower1], B, lower2, upper2) && gt_segs(A, lower1+1, upper1, B, lower2, upper2); } bool ge_segs(int[] A, int lower1, int upper1, int[] B, int lower2, int upper2) //@requires 0 <= lower1 && lower1 <= upper1 && upper1 <= \length(A); //@requires 0 <= lower2 && lower2 <= upper2 && upper2 <= \length(B); { if (lower1 == upper1) return true; return ge_seg(A[lower1], B, lower2, upper2) && ge_segs(A, lower1+1, upper1, B, lower2, upper2); } bool lt_segs(int[] A, int lower1, int upper1, int[] B, int lower2, int upper2) //@requires 0 <= lower1 && lower1 <= upper1 && upper1 <= \length(A); //@requires 0 <= lower2 && lower2 <= upper2 && upper2 <= \length(B); { if (lower1 == upper1) return true; return lt_seg(A[lower1], B, lower2, upper2) && lt_segs(A, lower1+1, upper1, B, lower2, upper2); } bool le_segs(int[] A, int lower1, int upper1, int[] B, int lower2, int upper2) //@requires 0 <= lower1 && lower1 <= upper1 && upper1 <= \length(A); //@requires 0 <= lower2 && lower2 <= upper2 && upper2 <= \length(B); { if (lower1 == upper1) return true; return le_seg(A[lower1], B, lower2, upper2) && le_segs(A, lower1+1, upper1, B, lower2, upper2); }