CSE 331: Section 4 — Loop Invariants & 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 this
     * @effects this is unchanged if this_0 contains n
     *          otherwise, this contains all of this_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 — Everybody Loops

In this problem, we will show the correctness of a method containing a loop that finds the quotient of \(x\) divided by 10, i.e., the largest value \(y\) such that \(10y \le x\). To say that \(y\) is the largest such value means that any larger value would not satisfy the inequality, i.e., that \(10(y+1) \not\le x\).

We denote the initial value of the parameter \(x\) at the top of the method by \(x_0\). This is explicitly stated in the precondition as the fact “\(x = x_0\)” (note this is not strictly necessary - you always know \(x = x_0\) until you modify it!). The first two facts of Q are from the spec postcondition, which say that \(y\) is the quotient of \(x_0\) divided by 10. The third fact is specific to our implementation, and says that \(x\) is the remainder, i.e., the remaining amount not divisible by 10.

This method calculates the quotient without division. Instead, it just uses subtraction. It operates by increasing y and decreasing x each time around. The first part of the invariant says that the distance from \(x_0\) down to \(10y\) (i.e., \(x_0 - 10y\)) is the same as the distance from \(x\) down to 0 (i.e., \(x - 0 = x\)). The second part of the invariant says that \(x\) has not moved below 0 (i.e., \(x \ge 0\)).

// Computes the integer quotient of x divided by 10
// @param x The numerator
// @requires x >= 0
// @return The largest integer y such that 10 * y <= x_0
public static int divideByTen(int x) {
  {{ x = x_0 and x_0 >= 0 }}
  int y = 0;
  {{ P1: _________________________ }}
  {{ Inv: x_0 - 10y = x and x >= 0 }}
  while (x >= 10) {
    {{ _________________________ }}
    y = y + 1;
    {{ _________________________ }}
    x = x - 10;
    {{ P3: _________________________ }}
    {{ Q2: _________________________ }}
  }
  {{ P2: _________________________ }}
  {{ Q1: 10y <= x_0 and x_0 < 10(y+1) and x = x_0 - 10y }}
  return y;
}

Fill in P1, then show that the invariant is true when we get to the top of the loop the first time.

Forward reasoning tells us that P1: \(x = x_0\), \(x_0 \ge 0\), and \(y = 0\).

We must show both parts of the invariant using our facts from P1.

From P1, since x = x_0 and y = 0, we can subtract 10y from the right side, resulting in the first fact from the invariant: x_0 - 10y = x.

From P1, since x_0 >= 0 and x = x_0, we can substitute in for x_0, resulting in the second fact from the invariant: x >= 0.
Fill in P2, then show that Q1 holds when we exit the loop.

When we exit the loop, we know that P2: inv (\(x_0 - 10y = x\), \(x \ge 0\)), and \(x < 10\). We must show all parts of Q1 using our facts from P2.

From the invariant in P2, we know x_0 - 10y = x and x >= 0. Substituting x >= 0 into x_0 - 10y = x, and adding 10y to both sides results in the first fact in Q1: 10y <= x_0.

From P2, we know x_0 - 10y = x and x < 10. Substituting x < 10 into x_0 - 10y = x and adding 10y to both sides results in x_0 < 10y + 10, which can be rewritten to show the second fact of Q1: x_0 < 10(y + 1).

The third fact of Q1 is given to us in P2: x_0 - 10y = x.
Fill in Q2 (Hint: what do we know at the end of a loop?). Then, forward reason to P3. Show that P3 implies Q2, proving that the body of the loop is correct.
```
{{ x_0 - 10y = x and x >= 0 and x >= 10 }}
y = y + 1;
{{ x_0 - 10(y - 1) = x and x >= 0 and x >= 10 }}
x = x - 10;
{{ P3: x_0 - 10(y - 1) = (x + 10) and (x + 10) >= 0 and (x + 10) >= 10 }}
{{ Q2: Inv: x_0 - 10y = x and x >= 0 }}
```
We must show all parts of Q2 using our facts from P3.

From P3, we know x_0 - 10(y - 1) = x + 10. Multiplying through and subtracting 10 from both sides gives x_0 - 10y = x, which is the first part of the invariant from Q2.

From P3, we know x + 10 >= 10. Subtracting 10 from both sides gives x >= 0, which is the second party of the invariant from Q2.

Task 2 — Rally the Loops

In this problem, you will implement the following function.

/**
 * Writes over each copy of y in A with the value z.
 * @param A the array to replace values in
 * @param y the value to be replaced in A
 * @param z the value to replace y with in A
 * @modifies A
 * @effects A = A_0 with every instance of y replaced with a z
 */
public void replace(int[] A, int y, int z) { .. }

With each loop invariant below, fill in the missing parts of the code to make it correct with the given invariant.

int i = ____________________

// Inv: A[0 .. i] = A_0[0 .. i] with every y replaced with a z
// and A[i .. A.length] = A_0[i .. A.length]
while (________________________________________) {







}

int i = 0;

// Inv: A[0 .. i] = A_0[0 .. i] with every y replaced with a z
// and A[i .. A.length] = A_0[i .. A.length]
while ( i < A.length ) {
  if (A[i] == y) {
    A[i] = z;
  }
  i++;
}

int i = ____________________

// Inv: A[0 .. i] = A_0[0 .. i] and A[i .. A.length] = A_0[i .. A.length] with
// every y replaced with a z
while (________________________________________) {







}

int i = A.length;

// Inv: A[0 .. i] = A_0[0 .. i] and A[i .. A.length] = A_0[i .. A.length] with
// every y replaced with a z
while ( i > 0 ) {
  i--;
  if (A[i] == y) {
    A[i] = z;
  }
}

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 this = this.elems[0 .. size] means that this 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: this = this.elems[0 .. size]
      private int[] elems;
      private int size;

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

(3)   // AF: this = 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 this
   * @effects this is unchanged if this_0 contains n
   *          otherwise, this contains all of this_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.

Task 4 — 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 this? If not, why is that allowed when it says @modifies this?

@modifies says that add may or can modify this but it is not a promise that it does so. For example, in this case we know this 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 this.

MutableIntSet.add actually changes the abstract state (this) 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 this
     * @effects if this_0 contains n, this = this_0 with n removed.
     *          If this_0 does not contain n, this = this_0.
     * @returns true if this_0 contains n, false otherwise.
     */
    public boolean remove(int n);