CSE 331: Section 5 — Arrays (Solutions)

Task 1 — Tw-Y's Removed

Considering the following method specification:

/**
 * Removes all instances of an int from the provided array, writing
 * the remaining elements into the first j indicies and returning j.
 * @param y the int to remove
 * @param arr the array to remove from
 * @requires arr != null
 * @modifies arr
 * @effects arr[: j] holds all the non-y elements in arr
 * @returns j the length of the non-y elements in arr
 */
public static int remove(int[] arr, int y);

In this problem, we will check the correctness of the following code that implements remove.

public static int remove(int[] arr, int y) {
  int i = 0;
  int j = 0;
  {{ P1: ______________________________________________________________ }}
  {{ Inv: arr[: j] contains all non-y elements from arr_0[: i] and
          arr[i :] = arr_0[i :] and length of arr = length of arr_0 }}
  while (i != arr.length) {
      if (arr[i] == y) {
          {{ P2: ______________________________________________________ }}
          {{ Q2: ______________________________________________________ }}
      } else {
          {{ P3: ______________________________________________________ }}
          {{ Q3: ______________________________________________________ }}
          arr[j] = arr[i];
          j = j + 1;
      }
      i = i + 1;
  }
  {{ P4: ______________________________________________________________ }}
  {{ Post: arr[: j] contains all non-y elements in arr_0 }}
  return j;
}

Fill in P1 using forward reasoning and then prove that P1 implies Inv.
{{ P1: i = 0 and j = 0 (and arr = arr_0, optionally) }}

The first fact of Inv holds since:
```
arr[: j] = arr[: 0]                 since j = 0
          = nil
          = arr_0[: 0]
          = arr_0[: i]               since i = 0
```
Since j is 0, arr[: j] is the empty array. The same holds for i = 0, so arr_0[: i] is also the empty array. There cannot be any non-y elements in the empty array, so this fact clearly holds.

The second fact of Inv holds since:
```
arr[i :] = arr[0 :]           since i = 0
        = arr
        = arr_0                 since arr = arr_0
        = arr_0[0 :]
        = arr_0[i :]           since i = 0
```
Since i is 0, arr_0[i :] = arr_0. Since arr has not been modified, arr = arr_0. We know that arr_0 = arr_0[0 :], and so arr_0[i :] = arr[i :]

The third fact of Inv holds since:
```
length of arr = length of arr_0     since arr = arr_0
```
Since arr has not been reassigned, the length of arr = length of arr_0.
Fill in P4 using forward reasoning and then prove that P4 implies the postcondition.

{{ P4: Inv (arr[: j] contains all non-y elements from arr_0[: i] and arr[i :] = arr_0[i :] and length of arr = length of arr_0) and i = arr.length }}

This gives us the postcondition as:

Since i = arr.length and arr.length = arr_0.length, i = arr_0.length. Thus, arr_0[: i] = arr_0[: arr_0.length] = arr_0. Since we have that arr[: j] contains all non-y elements from arr_0[: i], we see that arr[: j] contains all non-y elements from arr_0.
Fill in P2 using forward reasoning and Q2 using backward. Then, prove that P2 implies Q2.

{{ P2: Inv (arr[: j] contains all non-y elements from arr_0[: i] and arr[i :] = arr_0[i :] and length of arr = length of arr_0) and i != arr.length, and arr[i] = y }}

{{ Q2: arr[: j] contains all non-y elements from arr_0[: i+1] and arr[i+1 :] = arr_0[i+1 :] and length of arr = length of arr_0 }}

The first part follows since:

Since arr[i :] = arr_0[i :], arr[i] = arr_0[i]. This gives us arr[i] = arr_0[i] = y, meaning arr_0[i] is not a non-y element. Since arr[: j] contains all non-y elements in arr_0[: i] and arr_0[i] = y, we also know that arr[: j] contains all non-y elements from arr_0[: i+1].

The second part of Q2 is implied by the second fact from P2 (since arr[i+1 :] is a sublist of arr[i :] and the same for arr_0).

The third fact is directly implied.
Fill in P3 using forward reasoning and Q3 using backward. Then, prove that P3 implies Q3.

{{ P3: Inv (arr[: j] contains all non-y elements from arr_0[: i] and arr[i :] = arr_0[i :] and length of arr = length of arr_0), and i != len(arr) and arr[i] != y }}

{{ Q3: (arr[: j] ++ arr[i] contains all non-y elements from arr_0[: i+1] and arr[i+1 :] = arr_0[i+1 :] and length of arr = length of arr_0) }}

The first fact follows since: Since arr[i :] = arr_0[i :], arr[i] = arr_0[i]. Thus, arr[i] = arr_0[i] != y and arr[i] must be included in the non-y elements for arr_0[: i+1]. Since arr[: j] contains all non-y elements from arr_0[: i], concatenating arr[: j] ++ arr[i] would also contains all non-y elements from arr_0[: i + 1]. Thus, fact 1 holds.

The second part of Q3 is implied by the second fact from P3 (since arr[i+1 :] is a sublist of arr[i :]).

The third fact is directly implied.

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_0[i : ]
while (________________________________________) {







}

int i = 0;

// Inv: A[0 : i] = A_0[0 : i] with every y replaced with a z
// and A[i : ] = A_0[i : ]
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_0[i : ] with
// every y replaced with a z
while (________________________________________) {







}

int i = A.length;

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

Task 3 — Test, Ice, Compression, Elevation

In this problem, we will write tests for various join functions.

First, consider a version of join, which does not mutate either argument:

/** 
 * Join the two given lists into a single one
 * @requires first != null, second != null
 * @returns first concatenated with second
*/ 
public static List<Integer> join(List<Integer> first, List<Integer> second) {
  List<Integer> newList = new ArrayList<>();
  newList.addAll(first);
  newList.addAll(second);
  return newList;
}

Fill in the missing parts of the following JUnit test for this version of join.

@Test
public void testJoin(){
  List<Integer> list1 = new ArrayList<>(Arrays.asList(1, 2));
  List<Integer> list2 = new ArrayList<>(Arrays.asList(3, 4));
  assertEquals(________________________, join(list1, list2));

  List<Integer> list3 = new ArrayList<>(Arrays.asList(1));
  List<Integer> list4 = new ArrayList<>(Arrays.asList(2, 3, 4));
  assertEquals(________________________, join(list3, list4));
}

Both blanks should say Arrays.asList(1, 2, 3, 4)

Next, consider the following version of join, which mutates first and does not return anything

/** 
 * Join the two given lists into a single one
 * @requires first != null, second != null
 * @requires first != second
 * @modifies first
 * @effects first is first_0 concatenated with second
*/ 
public static void join(List<Integer> first, List<Integer> second) {
  first.addAll(second);
}

Rewrite the JUnit test above to use this new definition of join on the same inputs as above.

@Test
public void testJoin(){
  List<Integer> list1 = new ArrayList<>(Arrays.asList(1, 2));
  List<Integer> list2 = new ArrayList<>(Arrays.asList(3, 4));
  join(list1, list2);
  assertEquals(Arrays.asList(1, 2, 3, 4), list1);

  List<Integer> list3 = new ArrayList<>(Arrays.asList(1));
  List<Integer> list4 = new ArrayList<>(Arrays.asList(2, 3, 4));
  join(list3, list4);
  assertEquals(Arrays.asList(1, 2, 3, 4), list3);
}

This version should be longer than before. Why is that the case?

Since the function doesn't return the answer (it instead modifies the list), we have to put the call to join on a different line than the call to assertEquals.

Finally, consider this version of join, which modifies both first and second.

/** 
 * Join the two given lists into a single one
 * @requires first != null, second != null
 * @modifies first, second
 * @effects first is first_0 concatenated with second, second = nil
 * @return first
*/ 
public static List<Integer> join(List<Integer> first, List<Integer> second) {
  while (!second.isEmpty()) {
    first.add(second.get(0));
    second.remove(0);
  }
  return first;
}

Rewrite the JUnit test again to properly test this new definition of join.

We need to test that both of the lists were properly updated. Furthermore, since we used a loop, we have to add in additional test cases to get loop coverage.

@Test
public void testJoin(){
  List<Integer> list1 = new ArrayList<>();
  List<Integer> list2 = new ArrayList<>();
  assertEquals(Arrays.asList(), join(list1, list2));
  assertEquals(Arrays.asList(), list1);
  assertEquals(Arrays.asList(), list2);

  List<Integer> list3 = new ArrayList<>(Arrays.asList(1));
  List<Integer> list4 = new ArrayList<>(Arrays.asList(2));
  assertEquals(Arrays.asList(1, 2), join(list3, list4));
  assertEquals(Arrays.asList(1, 2), list3);
  assertEquals(Arrays.asList(), list4);

  List<Integer> list5 = new ArrayList<>(Arrays.asList(1, 2, 3));
  List<Integer> list6 = new ArrayList<>(Arrays.asList(4, 5, 6));
  assertEquals(Arrays.asList(1, 2, 3, 4, 5, 6), join(list5, list6));
  assertEquals(Arrays.asList(1, 2, 3, 4, 5, 6), list5);
  assertEquals(Arrays.asList(), list6);
}

Imagine we replaced the spec for join in the part d with the following spec:

/** 
 * Join the two given lists into a single one
 * @requires first != null, second != null
 * @modifies first, second
 * @effects first is first_0 concatenated with second
 * @return first
*/

What would we need to change about our test cases?

We now cannot test the mutated value of 'second' since our specification does not specify how 'second' may be modified. Thus, all we can correctly test (or test at all really) is the value of 'first' and the return value. This is why writing specifications is important!