CSE 331: Section 5 — Midterm Review

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

1. Use forward reasoning to fill in assertion P1.

2. Explain how P1 implies the postcondition:

3. Use forward reasoning to fill in assertion P2.

4. Explain how P2 implies the precondition to the method call:

5. Use forward reasoning to fill in assertion P3.

6. Use backward reasoning to fill in assertion Q3.

7. Explain how P3 implies Q3:

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

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

2. Is spec B stronger, weaker, or incomparable to spec D? Briefly explain your answer:

3. Is spec A stronger, weaker, or incomparable to spec E? Briefly explain your answer:

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

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.

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

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

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

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.

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

2.   /**
      * 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++;
     }
   

3.   /**
      * 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;
     }
   

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

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

2. Explain how P0 implies the loop invariant:

3. Explain how P1 implies the postcondition:

4. Explain how P2 implies the loop invariant:

5. Explain how P3 implies 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.

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

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

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

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

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

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