CSE 331: Section 1 — Specifications (Solutions)

Task 1

Recall this example from lecture:

/**
 * 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)

and these possible ways to complete this spec:

// 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

Compare these 5 specs for strength by filling in the following table. Write an "S" if the spec on left (the row) is stronger than the spec on top (the column), a "W" if the left spec is weaker, and "---" if the specs are incomparable.

	A	B	C	D	E
A	X	W	W	W	W
B	S	X	---	S	---
C	S	---	X	S	---
D	S	W	W	X	---
E	S	---	---	---	X

A is weaker than everything else.
B is stronger than D, but incomparable with C and E.
C is stronger than D but incomparable with E.
D and E are also incomparable.

Task 2

Here we look at a few different specifications for a method with this signature:

/**
 * 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)

We use the notation a[i..j] to refer to the elements of an array a from index i (inclusive) to j (exclusive). So a[0..n] is the elements of a at indices 0, 1, ..., n-1.

// 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;

Fill in the following table explaining which implementations satisfy which specifications. In each cell, write "yes" or "no" to say whether the implementation satisfies the spec.

	A	B	C	D
1	N	N	Y	Y
2	Y	Y	N	Y
3	N	Y	N	Y
4	N	Y	N	N

Impl 1 removes all occurrences of x in a[0..n], leaving remaining elements in order.
- Doesn't satisfy A or B because they require only one occurrence to be removed
- Does exactly what C says
- Also satisfies D because D's precondition (no duplicates) means removing all occurrences is the same thing as removing one occurrence.
Impl 2 removes the first occurrence of x in a[0..n] by shifting everything left by one.
- Does exactly what A says
- Also satisfies B because B says "possibly reordered", but reordering is not required, and B doesn't care which occurrence is removed.
- Doesn't satisfy C because it requires all occurrences to be removed.
- Also satisfies D, since under D's precondition, the only occurrence of x is also the first occurrence of x.
Impl 3 removes the last occurrence of x in a[0..n] by shifting everything left by one.
- Doesn't satisfy A because A asks for the first occurrence to be removed, not the last.
- Satisfies B because B says "possibly reordered", but reordering is not required, and B doesn't care which occurrence is removed.
- Doesn't satisfy C because it requires all occurrences to be removed.
- Also satisfies D, since under D's precondition, the only occurrence of x is also the last occurrence of x.
Impl 4 overwrites the first occurrence of x with a copy of a[n-1]
- Doesn't satisfy A or D because they require relative order to be preserved, but now a[n-1] got moved into the relative position that used to be occupied by x.
- Satisfies B because B allows reordering as long as there is one fewer occurrence of x, which there is, because Impl 4 overwrote one.
- Doesn't satisfy C because C requires removing all occurrences of x.