CSE 331: Section 4 — ADTs

This section's questions concern the following ADT:

 /**
  * Represents a **mutable** integer set, or a collection of distinct integers.
  */
  public class MutableIntSet {
    /**
     * Determines whether n is in the set.
     * @param n the number to look for in the set
     * @return true if n is in the set, false otherwise
     */
    public boolean contains(int n);

    /**
     * Adds n to the set if not already present.
     * @param n the number to add to the new set.
     * @modifies this
     * @effects this is unchanged if this_0 contains n
     *          otherwise, this contains all of this_0 and n
     */
    public void add(int n);

    /**
     * Removes the desired int from the set.
     * @param n The int to remove
     * .... To complete in part d
     */
    public boolean remove(int n);
  }

Task 1 — Good News and Add News

Answer the following questions about the specification of MutableIntSet. Assume that T is an instance of this class whose abstract state is {1, 2, 3}.

1. Would T.add(3) actually change this? If not, why is that allowed when it says @modifies this?

2. Consider the following static method.

   /**
    * Adds n to the set if not already present.
    * @param old the set to add to
    * @param n the number to add to the new set.
    * @requires old is not null
    * @return a set with n and all of the elements of old.
    * If old.contains(n), the new set has all the same elements as 'old'.
    */
   public static MutableIntSet add(MutableIntSet old, int n);
   

   Now, consider a call T.add(4). Explain how the operation of MutableIntSet.add differs from that of a call to static add(T, 4) in terms of this.

3. What is the abstract state of \(T\) after the following code (This is forward reasoning.):

        T.add(4);
        T.add(2);
        T.add(0);
   

4. Write a specification for the method remove. You should have two cases - n is in the set, and n is not. Clearly explain how the abstract state changes after the method call and what is returned.

Task 2 — Rich AF

In this problem, we will return to the original specification of MutableIntSet, whose abstract state is a set of elements. We will consider three different concrete representations for it.

Note the notation for this = this.elems[0 .. size] means that this is the set containing the first size elements from this.elems just like how an ArrayList would work!

    public class MutableIntSetImpl implements MutableIntSet {

(1)   // AF: this = this.elems[0 .. size]
      private int[] elems;
      private int size;

(2)   // AF: this = this.elems[0 .. size]
      // RI: this.elems[0..size] contains no dups
      private int[] elems;
      private int size;

(3)   // AF: this = this.elems[0 .. size]
      // RI: this.elems[0..size] is sorted by <=
      private int[] elems;
      private int size;

      public MutableIntSetImpl() {
        this.elems = new int[10];
        this.size = 0;
      }

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

1.   public boolean contains(int n) {
       return Arrays.binarySearch(this.elems, 0, this.size, n) >= 0;
     }
   

   Note: Binary Search is an algorithm that finds the position of a target value within a sorted array.

2.   /**
      * Determines whether n is in the set.
      * @param n the number to look for in the set
      * @return true if n is in the set, false otherwise
      */
     public boolean contains(int n) {
       for (int i = 0; i < this.size; i++) {
         if (this.elems[i] == n)
           return true;
       }
       return false;
     }
   

3.   /**
      * Adds n to the set if not already present.
      * @param n the number to add to the new set.
      * @modifies this
      * @effects this is unchanged if this_0 contains n
      *          otherwise, this contains all of this_0 and n
      */
     public void add(int n) {
       if (!this.contains(n)) {
         if (size >= this.elems.length) {
           int[] temp = new int[size * 2 + 1];
           for (int i = 0; i < this.elems.length; i++) {
             temp[i] = this.elems[i];
           }
           this.elems = temp;
         }
         this.elems[size] = n;
         size++;
       }
     }
   

4.   /**
      * Removes the desired int from the set.
      * @param n The int to remove
      * .... Based on your Task 1 part d solution
      */
     public boolean remove(int n) {
       for (int i = 0; i < size; i++) {
         if (this.elems[i] == n) {
           size--;
           for (int j = i; j < size; j++) {
             this.elems[j] = this.elems[j + 1];
           }
           return true;
         }
       }
       return false;
     }
   

Task 3 — Almond Joy

1. Use forward reasoning and known facts to fill in the blank.

   // AF: AF(this) = this.snacks[0 .. size] and top = this.snacks[size - 1]
   // RI: 0 <= this.size <= this.snacks.length
   /**
    * 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 0 <= size <= snacks.length AND size <= size_0 }}
     while (size != 0) {
       {{ _____________________________________________________________ }}
       String top = this.snacks[size - 1];
       if (top.equals("Almond Joy")) {
         {{ P1: _____________________________________________________________ }}
         return true;
       }
       {{ _____________________________________________________________ }}
       size--;
       {{ P2: _____________________________________________________________ }}
     }
     {{ P3: _____________________________________________________________ }}
     return false;
   }
   

2. Loop check(1) - Explain how P0 implies Inv:

   {{ P0: _____________________________________________________________ }}
   
   {{ Inv: this.snacks[size .. size_0] does not contain "Almond Joy"
     AND 0 <= size <= snacks.length AND size <= size_0 }}
   

3. Explain how P1 implies the postcondition:

   {{ P1: _____________________________________________________________ }}
   
   
   // @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
   

4. Loop check(2) - Explain how P2 implies the loop invariant:

   {{ P2: _____________________________________________________________ }}
   
   {{ Inv: this.snacks[size .. size_0] does not contain "Almond Joy"
   and 0 <= size and size <= snacks.length and size <= size_0 }}
   

5. Loop check(3) - Explain how P3 implies the postcondition:

   {{ P3: _____________________________________________________________ }}
   
   // @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