CSE 331: Section 4 — Mutable Specs & Data Abstraction (Solutions)

This section's questions concern the following ADT:

 /**
  * Represents a **mutable** integer set, or a collection of distinct integers.
  */
  public class MutableIntSet {
    /**
     * Determines whether n is in the set.
     * @param n the number to look for in the set
     * @return true if n is in the set, false otherwise
     */
    public boolean contains(int n);

    /**
     * Adds n to the set if not already present.
     * @param n the number to add to the new set.
     * @modifies obj
     * @effects obj is unchanged if obj_0 contains n
     *          otherwise, obj contains all of obj_0 and n
     */
    public void add(int n);

    /**
     * Removes the desired int from the set.
     * @param n The int to remove
     * .... To complete in part d
     */
    public boolean remove(int n);
  }

Task 1 — Good News and Add News

Answer the following questions about the specification of MutableIntSet. Assume that T is an instance of this class whose abstract state is {1, 2, 3}.

Would T.add(3) actually change obj? If not, why is that allowed when it says @modifies obj?

@modifies says that add may or can modify obj but it is not a promise that it does so. For example, in this case we know obj would not be modified (via its spec) since the set already contains 3.
Consider the following static method:
```
/**
 * Adds n to the set if not already present.
 * @param old the set to add to
 * @param n the number to add to the new set.
 * @requires old is not null
 * @return a set with n and all of the elements of old.
 * If old.contains(n), the new set has all the same elements as 'old'.
 */
public static MutableIntSet add(MutableIntSet old, int n);
```
Now, consider a call T.add(4). Explain how the operation of MutableIntSet.add differs from that of a call to static add(T, 4) in terms of obj.

MutableIntSet.add actually changes the abstract state (obj) to contain n, whereas the static (immutable) add method returns a new set and implicitly promises not to modify old by not having an @modifies clause.
What is the abstract state of \(T\) after the following code (This is forward reasoning.):
```
     T.add(4);
     T.add(2);
     T.add(0);
```
The resulting state would be {\(0, 4, 1, 2, 3\)}.

Write a specification for the method remove. You should have two cases - n is in the set, and n is not. Clearly explain how the abstract state changes after the method call and what is returned.

This is one possible solution:

    /**
     * Removes the desired int from the set. Returns true if successful,
     * false if the int isn't in this set.
     * @param n The int to remove.
     * @modifies obj
     * @effects if obj_0 contains n, obj = obj_0 with n removed.
     *          If obj_0 does not contain n, obj = obj_0.
     * @returns true if obj_0 contains n, false otherwise.
     */
    public boolean remove(int n);

Task 2 — Comparison is the Thief of Join

We plan to provide the following method:

    /**
     * Joins the two given MutableIntSet's into a single one.
     * @param first The first MutableIntSet
     * @param second The second MutableIntSet
     * @requires first and second are not null
     * ....
     */
    public MutableIntSet join(MutableIntSet first, MutableIntSet second);

To do so, we need to fill in the rest of the specification.

We are considering the following alternatives:

@return a set with all distinct elements from first and second           // Spec A

@modifies first                                                          // Spec B
@return a set with all distinct elements from first_0 and second

@modifies first, second                                                  // Spec C
@return a set with all distinct elements from first_0 and second_0

@modifies first                                                          // Spec D
@effects first = a set with all distinct elements from first_0 and second
@return a set with all distinct elements from first_0 and second

@modifies first, second                                                  // Spec E
@effects first = a set with all distinct elements from first_0 and second_0
@return a set

Fill in the following table explaining the relationships between each pair of specifications. 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 S S --- ---

B W X S W ---

C W W X W ---

D --- S S X S

E --- --- --- W X
- A is stronger than B and C as the lack of a @modifies clause is a promise not to modify anything, whereas an @modifies without an @effects simply means the spec may modify but doesn't specify how.
- A and D/E are incomparable as neither imply the other.
- B is stronger than C because C contains all of its @modifies and more.
- B is weaker than D because D specifies how first is modified, where B just says first may be modified.
- B is incomparable with E because B has a stronger postcondition from @modifies (promises to modify less), but E has a stronger postcondition from @effects (promises to modify first in a specific way). Neither imply the other.
- C is weaker than D because it modifies more and D specifies how it modifies first.
- C is incomparable with E because E specifies how first is modified in its @effects but has a less specific return statement.
- D is stronger than E because E contains all of its @modifies and more.
Not every combination of @modifies, @effects, and @return behaviors appearing in the previous specifications would be sensible. For example, consider the following specification:
```
/**
 * Joins the two given MutableIntSet's into a single one.
 * @param first The first MutableIntSet
 * @param second The second MutableIntSet
 * @requires first and second are not null
 * @effects first = a set with all unique elements from first_0 and second
 * @return a set with all unique elements from first_0 and second
 */
```
This specification is not sensible, what is wrong with it? Why shouldn't we use it?

The lack of a @modifies means the specification promises not to modify anything. However, the @effects states that it will modify first. These statements are contradictory.
(Bonus) If we remove the subscripts for first_0 or second_0 in the @return clause for specs B and C, they become incomparable with D/E (and likely don't mean what we want them to mean).
```
@modifies first, second                                        // Spec C
@return a set with all distinct elements from first and second
```
Explain why.
Without the subscript for first_0 or second_0, the returned set contains distinct elements from the current versions of first and second. Since we include those two sets in our @modifies but don't have an @effects outlining _how_ they are modified, first and second may have been changed from first_0 or second_0, meaning the returned set does not necessarily equal the set with all distinct elements of the two input sets (which is likely what we want). This uncertainty in the return means B/C would be incomparable with D/E, as they return different things and neither of which is definitively stronger (or implies the other).

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

Task 3 — RIch AF

In this problem, we will return to the original specification of MutableIntSet, whose abstract state is a set of elements. We will consider three different concrete representations for it (Note: the notation for obj = this.elems[0 : size] means that obj is the set containing the first size elements from this.elems just like how an ArrayList would work!):

    public class MutableIntSetImpl implements MutableIntSet {

(1)   // AF: obj = this.elems[0 : size]
      private int[] elems;
      private int size;

(2)   // AF: obj = this.elems[0 : size]
      // RI: this.elems contains no dups
      private int[] elems;
      private int size;

(3)   // AF: obj = this.elems[0 : size]
      // RI: this.elems is sorted
      private int[] elems;
      private int size;

      public MutableIntSetImpl() {
        this.elems = new int[10];
        this.size = 0;
      }

For each of the methods shown below, state the concrete representations (1--3) for which it would satisfy the specification of the method in MutableIntSet. In each case, briefly explain why.

```
  public boolean contains(int n) {
    return Arrays.binarySearch(this.elems, n) >= 0;
  }
```
Note: Binary Search is an algorithm that finds the position of a target value within a sorted array.

This implementation satisfies the specification only with concrete representation (3). When the array is not sorted, binarySearch is not guaranteed to find the element when present.

  /**
   * Determines whether n is in the set.
   * @param n the number to look for in the set
   * @return true if n is in the set, false otherwise
   */
  public boolean contains(int n) {
    for (int i = 0; i < this.size; i++) {
      if (this.elems[i] == n)
        return true;
    }
    return false;
  }

This implementation satisfies the specification with any of the concrete representations because it does not require any representation invariant to hold.

  /**
   * Adds n to the set if not already present.
   * @param n the number to add to the new set.
   * @modifies obj
   * @effects obj is unchanged if obj_0 contains n
   *          otherwise, obj contains all of obj_0 and n
   */
  public void add(int n) {
    if (!this.contains(n)) {
      if (size >= this.elems.length) {
        int[] temp = new int[size * 2 + 1];
        for (int i = 0; i < this.elems.length; i++) {
          temp[i] = this.elems[i];
        }
        this.elems = temp;
      }
      this.elems[size] = n;
      size++;
    }
  }

This satisfies the specification of add with concrete representations (1--2). This holds trivially for (1) since it has no representation invariant, and it holds with (2) because this implementation ensures no duplicates. It would not satisfy the spec with concrete representation (3) because it does not ensure that the array is sorted.

  /**
   * Removes the desired int from the set.
   * @param n The int to remove
   * .... Based on your Task 1 part d solution
   */
  public boolean remove(int n) {
    for (int i = 0; i < size; i++) {
      if (this.elems[i] == n) {
        size--;
        for (int j = i; j < size; j++) {
          this.elems[j] = this.elems[j + 1];
        }
        return true;
      }
    }
    return false;
  }

This satisfies the specification with concrete representations (2). It works with (2) because removing an element preserves the fact that there are no duplicates. It also preserves the sorting property required by (3); however, it still does not work with (3) or (1) because removing a single element does not leave an array not containing the element if there was more than one copy in the array.