CSE 331: Section 5 — Arrays

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

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

1. Fill in P1 using forward reasoning and then prove that P1 implies Inv.

2. Fill in P4 using forward reasoning and then prove that P4 implies the postcondition.

3. Fill in P2 using forward reasoning and Q2 using backward. Then, prove that P2 implies Q2.

4. Fill in P3 using forward reasoning and Q3 using backward. Then, prove that P3 implies Q3.

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) { .. }

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

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

Task 3 — Test, Ice, Compression, Elevation

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

1. 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));
   }
   

2. 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.

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

4. 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.

5. 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?