CSE 331: Section 1 — Specifications

/**
 * Searches for an element in a range of indices.
 * @param a the array to search, must be non-null
 * @param lo the (inclusive) low end of the range to search
 * @param hi the (exclusive) high end of the range to search
 * @param x the value to search for
 * ... more tags given below ...
 */
public static int indexOf(int[] a, int lo, int hi, int x)

// Spec A
// @requires 0 <= lo <= hi <= a.length and x occurs in a[lo..hi]
// @return an index i such that lo <= i < hi and a[i] == x

// Spec B
// @requires 0 <= lo <= hi <= a.length
// @return the *smallest* index i with lo <= i < hi and a[i] == x,
//          or -1 if no such index exists

// Spec C
// @requires 0 <= lo <= hi <= a.length
// @return the *largest* index i with lo <= i < hi and a[i] == x,
//          or -1 if no such index exists


// Spec D
// @requires 0 <= lo <= hi <= a.length
// @return *some* index i with lo <= i < hi and a[i] == x,
//          or -1 if no such index exists

// Spec E
// @requires 0 <= lo <= hi <= a.length
// @return the smallest index i with lo <= i < hi and a[i] == x
// @throws NoSuchElementException if no such index exists

/**
 * Removes x from the prefix a[0..n] (but see below for details)
 *
 * @param a the non-null array to remove from
 * @param n the length of the prefix
 * @param x the value to remove
 * @requires 0 <= n <= a.length
 * @modifies a
 */
public static int removeValue(int[] a, int n, int x)

// Spec A
// @effects if x does not occur in a[0..n], leaves a unchanged;
//   otherwise, if the first occurrence of x in a[0..n] is at index i,
//   then the new values in a[0..n-1] will be the old values of a[0..i]
//   followed by the old values of a[i+1..n], and the new value of a[n-1]
//   is unspecified. 
// @return n - 1 if x was removed, else n

// Spec B
// @effects if x does not occur in a[0..n], leaves a unchanged;
//   otherwise, the new values in a[0..n-1] are a possibly reordered version
//   of the old values of a[0..n] with one fewer occurrence of x,
//   and the new value of a[n-1] is unspecified
// @return n - 1 if x was removed, else n

// Spec C
// @effects if x does not occur in a[0..n], leaves a unchanged;
//   otherwise, if x occurs k > 0 times in a[0..n], then remove all k
//   occurrences of x, leaving remaining elements in the same relative
//   order as before; the new value of elements in a[n-k..n] is unspecified
// @return n - k

// Spec D
// @requires a[0..n] contains no duplicates
// @effects if x does not occur in a[0..n], leaves a unchanged;
//   otherwise, if x occurs in a[0..n] at index i, then the new values
//   in a[0..n-1] will be the old values of a[0..i] followed by the
//   old values of a[i+1..n], and the new value of a[n-1] is unspecified.
// @return n - 1 if x was removed, else n

// Impl 1
int w = 0;
for (int r = 0; r < n; r++) {
    if (a[r] != x) {
        a[w] = a[r];
        w++;
    }
}
return w;

// Impl 2
for (int i = 0; i < n; i++) {
    if (a[i] == x) {
        for (int k = i; k < n - 1; k++) {
            a[k] = a[k + 1];
        }
        return n - 1;
    }
}
return n;

// Impl 3
for (int i = n - 1; i >= 0; i--) {
    if (a[i] == x) {
        for (int k = i; k < n - 1; k++) {
            a[k] = a[k + 1];
        }
        return n - 1;
    }
}
return n;

// Impl 4
for (int i = 0; i < n; i++) {
    if (a[i] == x) {
        a[i] = a[n - 1];
        return n - 1;
    }
}
return n;