CSE 331: Section 6 — Midterm Review

Task 1 - With Great Power Comes Great Snacking

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. Show that P1 implies the postcondition:

3. Use forward reasoning to fill in assertion P2.

4. Show that 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. Show that P3 implies Q3:

The remaining questions concern the following ADT:

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

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

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

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

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

Task 2 — Snack Comparison

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 obj must contain only "Hot Pocket"s and not be empty       // Spec A
@modifies obj
@return a list with all snacks eaten from snack overflow

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

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

@return a list of strings                                            // Spec D

@requires obj must not be empty                                      // Spec E
@modifies obj
@effects empties obj
@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 obj
     * @effects removes snack from obj
     */
     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 obj
    * @effects obj = obj_0 with all copies of snack removed
    * @return the number of copies of snack removed from obj_0,
    *   or 0 if snack did not appear in obj_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 — Reppermint Tea

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: obj = this.snacks[0 : size]
      // RI: 0 <= this.size <= this.snacks.length

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

(3)   // AF: obj = 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 obj is not empty
      * @modifies obj
      * @effects obj is obj_0 without the topmost element
      * @return the snack popped from the top of obj_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 obj
      * @effects obj is obj_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 obj
      * @effects obj is empty
      * @return a list containing all snacks that were in obj_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 obj until an "Almond Joy" is encountered.
 * The "Almond Joy" is not removed.
 * @modifies obj
 * @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. Show that P0 implies the loop invariant:

3. Show that P1 implies the postcondition:

4. Show that P2 implies the loop invariant:

5. Show that P3 implies the postcondition:

Task 6 — Repperoni Pizza Minis

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

// AF: obj = 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 obj
   * @effects obj = obj_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 — Test Protein Chips

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

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

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.

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