CSE 331: Section 5 — Midterm Review (Solutions)

Task 1 - With Great Power Comes Great Reasonability

For this problem, we'll prove that the following recursive method is correct using Floyd reasoning

/**
* Returns base to the power of exp
* @param base the base
* @param exp the exponent to raise base to
* @requires exp >= 0
* @return base^exp
*/
public static int power(int base, int exp) {
  {{____________________________________________}}
  if (exp == 0) {
    {{P1:_______________________________________}}
    return 1;
  }
  {{P2:_________________________________________}}
  int temp = power(base, exp - 1);
  {{P3:_________________________________________}}
  {{Q3:_________________________________________}}
  int ans = base * temp;
  {{____________________________________________}}
  return ans;
}

Use forward reasoning to fill in assertion P1.

{{P1: exp >= 0 and exp = 0 }} \(\leftrightarrow\) {{P1: exp = 0 }}
Explain how P1 implies the postcondition:

We know that for any base, \(\text{base}^{0} = 1\). Since we know that exp = 0, returning 1 here satisfies the post condition.
Use forward reasoning to fill in assertion P2.

{{P2: exp >= 0 and exp != 0 }} \(\leftrightarrow\) {{P2: exp > 0 }}
Explain how P2 implies the precondition to the method call:

We know that exp > 0 so by subtracting 1 from both sides, we get exp - 1 > -1. We can re-write this into exp - 1 >= 0 since exp is an integer. Since we're passing in exp - 1 into the recursive call's exp parameter and exp - 1 >= 0, we have satisfied the precondition.
Use forward reasoning to fill in assertion P3.

{{P3: exp > 0 and temp = base^(exp - 1)}}
Use backward reasoning to fill in assertion Q3.

{{Q3: base * temp = base^exp}}
Explain how P3 implies Q3:

If we take our second fact in P3 (\(\text{temp} = \text{base}^{\text{exp} - 1}\)) and multiply both sides by \(\text{base}\), we get Q3. The right hand side becomes \(\text{base} * \text{base}^{\text{exp} - 1}\) which can be simplified to \(\text{base}^\text{exp}\).

The remaining questions concern the following ADT:

 /**
  * Represents a **mutable** stack of Strings representing snacks.
  */
  public class SnackOverflow {
    /**
     * Checks if this is empty
     * @return true if this is empty (cries), false otherwise
     */
    public boolean isEmpty();

    /**
     * Adds snack to the top of snack overflow
     * @param snack the snack to add
     * @modifies this
     * @effects this is this_0 with snack added to the top
     */
    public void pushSnack(String snack);

    /**
     * Removes the topmost snack in snack overflow to consume
     * @requires this is not empty
     * @modifies this
     * @effects this is this_0 without the topmost element
     * @return the snack popped from the top
     */
    public String popSnack();

    /**
     * Consumes all snacks in Snack Overflow (Kyle or Raio
     * must have come by...)
     * .... Task 2
    public List<String> consumeAll();

    /**
     * .... Task 3
    public ???? removeAll();
  }

Task 2 — Battle of the Bites

We plan to provide the following method

/**
* Consumes all snacks in Snack Overflow
* ....
*/
public List<String> consumeAll();

To do so, we need to fill in the rest of the specification. We are considering the following alternatives:

@requires this must contain only "Hot Pocket"s and not be empty       // Spec A
@modifies this
@return a list with all snacks eaten from snack overflow

@requires this must not be empty                                      // Spec B
@modifies this
@return a list with all snacks eaten from snack overflow

@modifies this                                                        // Spec C
@effects empties this
@return a list with all snacks eaten from snack overflow

@return a list of strings                                             // Spec D

@requires this must not be empty                                      // Spec E
@modifies this
@effects empties this
@return a list with all snacks eaten from snack overflow

Is spec B stronger, weaker, or incomparable to spec C? Briefly explain your answer:

Spec B is weaker than spec C. Since Spec B has an @requires clause and spec C does not, spec B has stronger precondition than spec C. Additionally, since both specs have an @modifies clause but only spec C defines the modification behavior with its @effects clause, spec B has a weaker postcondition than spec C. Since spec B has a stronger precondition and a weaker postcondition, it is a weaker spec than spec C.
Is spec B stronger, weaker, or incomparable to spec D? Briefly explain your answer:

Spec B is incomparable to spec D. Spec B's postcondition is incomparable to spec D as the @modifies clause in spec B makes the postcondition weaker while the @return clause makes the postcondition stronger in spec B as it describes what list of Strings is returned.
Is spec A stronger, weaker, or incomparable to spec E? Briefly explain your answer:

Spec A is weaker than spec E. Spec A's precondition is stronger as it places more requirements in the @requires clause. Spec A's postcondition is weaker as it lacks the @effects clause defining the behavior for what modifications occur to this. Since A has a stronger precondition and a weaker postcondition, it is a weaker spec.
Suppose we initially went with Spec A. Eventually, Distinguished Engineers Isayiah and Lawrence got tired of eating just Hot Pockets and decided to switch the implementation to spec C. Between the clients and the implementers, who is happy and who is sad about this change?

Spec A is a weaker spec to spec C as it has a stronger precondition and a weaker postcondition. Therefore, the clients are happy as they don't need to change their code. The implementers however are sad as they need to rewrite the method (and they loved the hot pockets).

Task 3 — Specs Mix

This question will continue to refer to the SnackOverflow ADT. Now that SnackOverflow is up and running, the creators are trying to add a little more functionality. They're thinking of adding some sort of removeAll function that removes all occurrences of a given snack from the stack, but otherwise maintains the order.

Consider this initial draft for removeAll:
```
  /**
  * Removes snack from this SnackOverflow.
  * @param snack the snack to remove
  * @modifies this
  * @effects removes snack from this
  */
  public void removeAll(String snack);
```
Identify two or more things that are unspecified or ambiguous, briefly explain why each is a problem.

It's unspecified what happens if there are no instances of snack, should the stack be unchanged? Should an exception be thrown? It also just says "remove snack" in our spec. What if there are multiple instances? From the written spec, we don't know if we should remove all or just one of the snacks we see.

Now consider a version of the function that actually returns something. Write a valid Javadoc specification for a version of removeAll that returns a List<Integer> with all the positions where the snack was removed.

/**
 * @param snack non-null snack to remove
 * @modifies this
 * @effects this = this_0 with all copies of snack removed
 * @return a List of the positions (0 = bottom of this_0) of every
 *   removed snack, in bottom-to-top order; empty list if none found
 */
public List<Integer> removeAll(String snack);

There are other possible specs as well, this is just an example!

Now, consider yet another version of removeAll that returns an int:

/**
 * Removes all occurrences of snack from this SnackOverflow.
 * @param snack the snack to remove
 * @modifies this
 * @effects this = this_0 with all copies of snack removed
 * @return the number of copies of snack removed from this_0,
 *   or 0 if snack did not appear in this_0
 */
public int removeAll(String snack);

Given this specification, write a different specification that is incomparable to this original one. Your spec must have the same method signature. Briefly justify why they're incomparable.

/**
 * Removes all occurrences of snack from this SnackOverflow.
 * @param snack the snack to remove
 * @modifies this
 * @effects this = this_0 with all copies of snack removed
 * @return 1 if the snack appeared in this_0, 0 otherwise
 */
public int removeAll(String snack);

These have incomparable return statements, so they're incomparable overall!

Task 4 — Hungry AF

In this problem, we'll return to the original specification for SnackOverflow, whose abstract state is a stack of String elements representing snacks. We'll consider three different concrete representations for it.

    public class SnackOverflowImpl implements SnackOverflow {
(1)   // AF: AF(this) = this.snacks[0 .. size]
      // RI: 0 <= this.size <= this.snacks.length

(2)   // AF: AF(this) = this.snacks[0 .. size]
      // RI: 0 <= this.size <= this.snacks.length and this.snacks.length >= 10

(3)   // AF: AF(this) = this.snacks[snacks.length - size .. snacks.length]
      //     where snacks[snacks.length - size] is the top of the stack.
      // RI: 0 <= this.size <= this.snacks.length

      private String[] snacks;
      private int size;

      public SnackOverflowImpl() {
        this.snacks = new String[10];
        this.size = 0;
      }

      // ... method implementations below ...

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

  /**
   * Removes the topmost snack in snack overflow to consume
   * @requires this is not empty
   * @modifies this
   * @effects this is this_0 without the topmost element
   * @return the snack popped from the top of this_0
   */
  public String popSnack() {
    String popped = this.snacks[this.snacks.length - size];
    size--;
    return popped;
  }

This only satisfies the specification with concrete rep (3). It correctly reads the top element from snacks.length - size, matching the reversed AF. It fails for (1) and (2) because it reads from the wrong end of the physical array, returning garbage (or nulls) instead of the actual top element at size - 1.

  /**
   * Adds snack to the top of snack overflow
   * @param snack the snack to add
   * @modifies this
   * @effects this is this_0 with snack added to the top
   */
  public void pushSnack(String snack) {
    if (size >= this.snacks.length) {
      String[] temp = new String[size * 2 + 1];
      for (int i = 0; i < this.snacks.length; i++) {
        temp[i] = this.snacks[i];
      }
      this.snacks = temp;
    }
    this.snacks[size] = snack;
    size++;
  }

This satisfies the specification with concrete representations (1) and (2). It correctly maintains the capacity and bounds for the standard arrays. It fails for (3) because it assumes the stack grows from left to right. It places the new element at index size and copies elements to the front of the new array during resize, breaking the reversed AF.

  /**
   * Consumes all snacks in Snack Overflow
   * @modifies this
   * @effects this is empty
   * @return a list containing all snacks that were in this_0 (top to bottom)
   */
  public List<String> consumeAll() {
    List<String> eaten = new ArrayList<>();
    for (int i = size - 1; i >= 0; i--) {
      eaten.add(this.snacks[i]);
    }
    this.snacks = new String[0];
    this.size = 0;
    return eaten;
  }

This satisfies the specification only with concrete rep (1). It fails for (2) because setting this.snacks = new String[0] shrinks the array to length 0, violating the minimum capacity RI (>= 10). It fails for (3) because the loop iterates from size - 1 down to 0, reading from the wrong side of the physical array.

Task 5 — Almond Floyds

Consider this method and spec for removeUntil using Concrete Rep (1), which continues to remove snacks until an Almond Joy is found

/**
 * Removes snacks from the top of this until an "Almond Joy" is encountered.
 * The "Almond Joy" is not removed.
 * @modifies this
 * @effects removes all elements above the first occurrence of "Almond Joy"
 *          (from the top); if no "Almond Joy" exists, removes all elements
 * @return true if an "Almond Joy" was encountered, false otherwise
 */
public boolean removeUntil() {
  {{ P0: _____________________________________________________________ }}
  {{ Inv: this.snacks[size .. size_0] does not contain "Almond Joy" and size >= 0 }}
  while (size != 0) {
    {{ _____________________________________________________________ }}
    String top = this.snacks[size - 1];
    {{ _____________________________________________________________ }}
    if (top.equals("Almond Joy")) {
      {{ P1: _____________________________________________________________ }}
      return true;
    }
    {{ _____________________________________________________________ }}
    size--;
    {{ P2: _____________________________________________________________ }}
  }
  {{ P3: _____________________________________________________________ }}
  return false;
}

Use forward reasoning and what we originally know to fill out all the Ps.

/**
 * Removes snacks from the top of this until an "Almond Joy" is encountered.
 * The "Almond Joy" is not removed.
 * @modifies this
 * @effects removes all elements above the first occurrence of "Almond Joy"
 *          (from the top); if no "Almond Joy" exists, removes all elements
 * @return true if a "Almond Joy" was encountered, false otherwise
 */
public boolean removeUntil() {
  {{ P0: 0 <= this.size <= this.snacks.length and size = size_0 }}
  {{ Inv: this.snacks[size .. size_0] does not contain "Almond Joy"
          and size >= 0 }}
  while (size != 0) {
    {{ this.snacks[size .. size_0] does not contain "Almond Joy" and
       size > 0 }}
    String top = this.snacks[size - 1];
    if (top.equals("Almond Joy")) {
      {{ P1: this.snacks[size .. size_0] does not contain "Almond Joy"
             and size > 0 and top = this.snacks[size - 1] and
             top = "Almond Joy" }}
      return true;
    }
    size--;
    {{ P2: this.snacks[size + 1 .. size_0] does not contain "Almond Joy"
           and size + 1 > 0
             and top = this.snacks[size] and top != "Almond Joy" }}
  }
  {{ P3: this.snacks[size .. size_0] does not contain "Almond Joy"
         and size = 0 }}
  return false;
}

}

Explain how P0 implies the loop invariant:

The first part follows since:

Since size = size_0 (hasn't been modified), we can see that this.snacks[size .. size_0] = this.snacks[size_0 .. size_0] = nil. Since this contains no elements, it does not contain "Almond Joy".

The second part holds directly (which we got from the RI, which holds at the beginning of any method).
Explain how P1 implies the postcondition:

P1: this.snacks[size .. size_0] does not contain "Almond Joy" and size > 0 and top = this.snacks[size - 1] and top = "Almond Joy"

The postcondition has 2 parts - the @effects (removes all elements above the first occurrence of "Almond Joy" (from the top); if no "Almond Joy" exists, removes all elements) and the @return (true if a "Almond Joy" was encountered, false otherwise).

The @effects holds as

Since we only access elements using size, decrementing size in essence deletes them. Since this.snacks[size .. size_0] does not contain "Almond Joy", we know that all removed elements do not equal "Almond Joy". Since size > 0, we can safely index into size - 1 which is >= 0. This gives us top = this.snacks[size - 1] and top = "Almond Joy", meaning we have that top is the first instance of "Almond Joy" and we removed above it.

The holds as

Since size > 0, size - 1 >= 0. Thus we can index into this.snacks. Since top = this.snacks[size - 1] and top = "Almond Joy", we know that snacks contains "Almond Joy" and we should return true, which we do.
Explain how P2 implies the loop invariant:

P2: this.snacks[size + 1 .. size_0] does not contain "Almond Joy" and size + 1 > 0 and top = this.snacks[size] and top != "Almond Joy"

Since we have size > 0, we know we can index into this.snacks. From knowing top isn't "Almond Joy" and top = this.snacks[size], we know this.snacks[size] isn't "Almond Joy". We can use that alongside, this.snacks[size + 1 .. size_0] does not contain "Almond Joy", to get that this.snacks[size .. size_0] doesn't contain "Almond Joy".

For the second part, since size + 1 > 0, that's the same as size >= 0.
Explain how P3 implies the postcondition:

P3: this.snacks[size .. size_0] does not contain "Almond Joy" and size = 0

The postcondition has 2 parts - the @effects (removes all elements above the first occurrence of "Almond Joy" (from the top); if no "Almond Joy" exists, removes all elements) and the @return (true if a "Almond Joy" was encountered, false otherwise).

The @effects holds as

Since we only access elements using size, decrementing size in essence deletes them. Since this.snacks[size .. size_0] does not contain "Almond Joy", we know that all removed elements do not equal "Almond Joy". Since size = 0, we know that all elements in the stack have been removed.

The @return holds as

Since size = 0, we can't continue indexing to this.snacks since it's empty, and all other elements have been removed since they weren't "Almond Joy"s. So, we return false, fulfilling the postcondition.

Task 6 — Chicken Noodle Loop

Now, implement the following new method for Concrete Representation (1).

// AF: AF(this) = this.snacks[0 .. size]
// RI: 0 <= this.size <= this.snacks.length

  /**
   * Replaces all instances of a specific snack with a new one.
   * @param oldSnack the snack to be replaced
   * @param newSnack the value to replace oldSnack with
   * @requires oldSnack != null, newSnack != null
   * @modifies this
   * @effects this = this_0 with every instance of oldSnack replaced with newSnack
   */
  public void replaceSnack(String oldSnack, String newSnack) { ... }

With each loop invariant below, fill in the missing parts of the code to make it correct with the given invariant. Remember to use .equals() to compare strings.

  int i = ____________________;
  // Inv: this.snacks[0 .. i] = this.snacks_0[0 .. i] and
  // this.snacks[i .. size] = this.snacks_0[i .. size] with
  // every instance of oldSnack replaced with newSnack.
  while (________________________________________) {






  }

  int i = size;

  // Inv: this.snacks[0 .. i] = this.snacks_0[0 .. i] and
  // this.snacks[i .. size] = this.snacks_0[i .. size] with
  // every instance of oldSnack replaced with newSnack.
  while ( i > 0 ) {
    i--;
    if (oldSnack.equals(this.snacks[i])) {
      this.snacks[i] = newSnack;
    }
  }

  int i = ____________________;
  // Inv: this.snacks[i-1 .. size] = this.snacks_0[i-1 .. size] and
  // this.snacks[0 .. i-1] = this.snacks_0[0 .. i-1] with
  // every instance of oldSnack replaced with newSnack.
  while (________________________________________) {






  }

  int i = 1;

  // Inv: this.snacks[i-1 .. size] = this.snacks_0[i-1 .. size] and
  // this.snacks[0 .. i-1] = this.snacks_0[0 .. i-1] with
  // every instance of oldSnack replaced with newSnack.
  while (i <= size) {
    if (oldSnack.equals(this.snacks[i-1])) {
      this.snacks[i-1] = newSnack;
    }
    i++;
  }

Task 7 — Cinnamon Test Crunch

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

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

/**
 * Restocks SnackOverflow after hitting up Costco.
 * @requires main != null, backup != null
 * @returns a list containing all of main followed by all of backup
 */
public static List<String> restock(List<String> main, List<String> backup) {
  List<String> newList = new ArrayList<>();
  newList.addAll(main);
  newList.addAll(backup);
  return newList;
}

Fill in the missing parts of the following JUnit test for this version of restock.
```
@Test
public void testRestock(){
  List<String> list1 = new ArrayList<>(
      Arrays.asList("Chicken Bakes", "Hot Pockets"));
  List<String> list2 = new ArrayList<>(
      Arrays.asList("Pocky", "Celsius"));
  assertEquals(________________________________________,
               restock(list1, list2));

  List<String> list3 = new ArrayList<>(
      Arrays.asList("Chicken Bakes"));
  List<String> list4 = new ArrayList<>(
      Arrays.asList("Hot Pockets", "Pocky", "Celsius"));
  assertEquals(________________________________________,
               restock(list3, list4));
}
```
After writing your tests, justify your choices:
Which testing heuristic(s) did you use?
What behavior from the specification does your test check?

Both blanks should say Arrays.asList("Chicken Bakes", "Hot Pockets", "Pocky", "Celsius")

Justification:
Black-box testing: We are testing the behavior described by the specification. (We check that the returned list contains all elements from main followed by all elements from backup.)
Boundary cases: We tested different list sizes/orderings (such as when main only has one element).
Clear-box testing: Not necessary because there are no branches or loops in the implementation.

Next, consider the following version of restock, which mutates main and does not return anything:

/**
 * Restock the main stash with the backup stash.
 * @requires main != null, backup != null
 * @requires main != backup
 * @modifies main
 * @effects main is main_0 concatenated with backup
*/
public static void restock(List<String> main, List<String> backup) {
  if (!backup.isEmpty()) {
    main.addAll(backup);
  }
}

Rewrite the JUnit test above to use this new definition of restock on the same inputs as above. After writing your test, justify why these test cases are sufficient. Consider:
What implementation details changed?
What code coverage requirements do we need to satisfy?

@Test
public void testRestock(){
  // If branch & statement coverage
  List<String> list1 = new ArrayList<>(
      Arrays.asList("Chicken Bakes", "Hot Pockets"));
  List<String> list2 = new ArrayList<>(
      Arrays.asList("Pocky", "Celsius"));
  restock(list1, list2);
  assertEquals(Arrays.asList("Chicken Bakes",
      "Hot Pockets", "Pocky", "Celsius"), list1);

  // Implicit else branch for branch coverage
  List<String> list3 = new ArrayList<>();
  restock(list1, list3);
  assertEquals(Arrays.asList("Chicken Bakes",
      "Hot Pockets", "Pocky", "Celsius"), list1);
}

Justification:
Clear-box testing: The implementation contains an if statement, so we must test all paths through the code.
Statement coverage: We test both executing the addAll statement and skipping the if body.
Boundary cases: An empty backup list tests the edge of the conditional behavior.

Finally, consider this version of restock, which modifies both main and backup.

/**
 * Restock the main stash by emptying the backup stash.
 * @requires main != null, backup != null
 * @modifies main, backup
 * @effects main is main_0 concatenated with backup_0, backup is empty
 * @return main
*/
public static List<String> restock(List<String> main, List<String> backup) {
  while (!backup.isEmpty()) {
    main.add(backup.get(0));
    backup.remove(0);
  }
  return main;
}

Rewrite the JUnit test again to properly test this new definition of restock and justify your choices.

We need to test that both 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 testRestock(){
  // 0 iterations
  List<String> list1 = new ArrayList<>();
  List<String> list2 = new ArrayList<>();
  assertEquals(Arrays.asList(), restock(list1, list2));  // Test returns
  assertEquals(Arrays.asList(), list1);                  // Test side effects
  assertEquals(Arrays.asList(), list2);

  // 1 iteration
  List<String> list3 = new ArrayList<>(Arrays.asList("Chicken Bakes"));
  List<String> list4 = new ArrayList<>(Arrays.asList("Hot Pockets"));
  assertEquals(Arrays.asList("Chicken Bakes", "Hot Pockets"),
               restock(list3, list4));
  assertEquals(Arrays.asList("Chicken Bakes", "Hot Pockets"), list3);
  assertEquals(Arrays.asList(), list4);

  // 2+ iterations
  List<String> list5 = new ArrayList<>(
      Arrays.asList("Chicken Bakes", "Hot Pockets", "Pocky"));
  List<String> list6 = new ArrayList<>(
      Arrays.asList("Celsius", "Chicken Melts", "Green Tea"));
  assertEquals(Arrays.asList("Chicken Bakes", "Hot Pockets",
      "Pocky", "Celsius", "Chicken Melts", "Green Tea"),
      restock(list5, list6));
  assertEquals(Arrays.asList("Chicken Bakes", "Hot Pockets",
      "Pocky", "Celsius", "Chicken Melts", "Green Tea"), list5);
  assertEquals(Arrays.asList(), list6);
}

Justification:
Black-box testing: We must ensure the method satisfies the effects clause. In particular, we check that main contains the original elements from main_0 followed by backup_0, and that backup is empty.
Mutation testing: Since this method modifies both lists, we must check both modified lists instead of only checking the returned value.
Clear-box testing: The method contains a loop, so we need loop coverage.
Loop coverage:

0 iterations → backup starts empty.
1 iteration → one element is removed from backup.
2+ iterations → multiple elements are removed from backup.