Representation Invariants and Abstraction Functions

The goal for this recitation is to provide practice in using (and then inventing) Rep Invariants and Abstraction Functions for collection classes.

Priority Queue questions

The specification fields are elements (a set) and priority (a function from objects to doubles). The representation fields are a Vector heap and a HashSet elts. Each component of heap (except the first) is of type Entry, with fields key and value.

The representation invariant is

• Each component of heap (except the first) is of type Entry
• The components of heap (except the first) have different value fields. Mathematically we can write this as

  for all i and j with 1<=i<j<heap.size():
  heap.elems[i].value != heap.elems[j].value

  Note: this does not cover i=0 or j=0
• The key fields of the components of heap (except the first) are ordered in a complicated way: the key at index i is no bigger than the key fields at index 2i and 2i+1. Mathematically
  • for all i with 1<2*i<heap.size():
    heap.elems[i].key <= heap.elems[2*i].key
  • for all i with 1<2*i+1<heap.size():
    heap.elems[i].key <= heap.elems[2*i+1].key
• The set elts is the same as the set of value fields for the components of heap other than the first; mathematically

  for every x, x is in elts if and only if there exists i with 1 <= i < heap.size() and x = heap.elems[i].value

• The heap vector has at least one element. (However, the first element of heap is arbitrary -- it is ignored in all the code.)

  heap.size() >= 1

The abstraction function is that

• elements is the set of heap.elems[i].value for 1 <= i < heap.size(),
• priority is the (partial) function whose value at x is heap.elems[i].key if (x=heap.elems[i].value) and (1<=i<heap.size())

In writing out descriptions of this data structure, we will use a textual notation. Here we write the entry y as a pair (y.key, y.value), we write the Vector as an array [e1, e2, e3...], and we use distinct symbols o1, o2 , o3 for distinct objects

• When extractMin() is called on the object whose representation is heap = [o1, (3.0, o2), (6.0, o3), (4.0, o4), (8.0, o5), (10.0, o6), (7.0, o7), (5.0, o8)], elts = {o2, o3, o4, o5, o6, o7, o8}, the code gradually transforms the state, through the following intermediate situations, to the final state shown.
  • at the start of extractMin(),

    heap = [o1, (3.0, o2), (6.0, o3), (4.0, o4), (8.0, o5), (10.0, o6), (7.0, o7), (5.0, o8)],
    elts = {o2, o3, o4, o5, o6, o7, o8},

  • after elts.remove(min),

    heap = [o1, (3.0, o2), (6.0, o3), (4.0, o4), (8.0, o5), (10.0, o6), (7.0, o7), (5.0, o8)],
    elts = {o3, o4, o5, o6, o7, o8},

  • after heap.setElementAt(...),

    heap = [o1, (5.0, o8), (6.0, o3), (4.0, o4), (8.0, o5), (10.0, o6), (7.0, o7), (5.0, o8)],
    elts = {o3, o4, o5, o6, o7, o8},

  • after heap.removeElementAt(...), before calling heapify(1) which is a private method of PriorityQueue

    heap = [o1, (5.0, o8), (6.0, o3), (4.0, o4), (8.0, o5), (10.0, o6), (7.0, o7)]
    elts = {o3, o4, o5, o6, o7, o8},

  • just before the recursive call heapify(3)

    heap = [o1, (4.0, o4), (6.0, o3), (5.0, o8), (8.0, o5), (10.0, o6), (7.0, o7)]
    elts = {o3, o4, o5, o6, o7, o8},

  • at the end of the whole method extractMin() which returns o2

    heap = [o1, (4.0, o4), (6.0, o3), (5.0, o8), (8.0, o5), (10.0, o6), (7.0, o7)]
    elts = {o3, o4, o5, o6, o7, o8},

  For each concrete state shown above, say whether or not it satisfies the representation invariant. Hint: some of these concrete states do not satisfy the invariant.
• As the example above shows, the concrete state does not satisfy the representation invariant at all times during the execution of the method. In particular, it is possible that the invariant is false just before calling heapify. What lesson does this have for reasoning about methods, and for using checkRep as a debugging tool?
• Give the abstract state corresponding to the first and last concrete states in this sequence. Is this compatible with the specification for extractMin which is

       * @returns elt such that elt is in this.elements
       *        && for all elt2 in this.elements, priority(elt) <= priority(elt2)
       * @effects removes elt from this.elements and from the domain of priority
       * @throws NoSuchElementException if this.elements is empty
  

• Find another concrete state which satisfies the representation invariant, and represents the same abstract state as the concrete state shown above after extractMin().
• Below we show the state at various stages during a call to extractMin(), if it were executed starting from a state which does not satisfy the representation invariant, but still has the same abstract state (given by the abstraction function) as the starting state above. How would a client see something wrong in this?
  • at the start of extractMin()

    heap = [o1, (4.0, o4), (6.0, o3), (8.0, o5), (3.0, o2), (10.0, o6), (7.0, o7), (5.0, o8)],
    elts = {o2, o3, o4, o5, o6, o7, o8},

  • after elts.remove(min)

    heap = [o1, (4.0, o4), (6.0, o3), (8.0, o5), (3.0, o2), (10.0, o6), (7.0, o7), (5.0, o8)],
    elts = {o2, o3, o5, o6, o7, o8},

  • after heap.setElementAt(...),

    heap = [o1, (5.0, o8), (6.0, o3), (8.0, o5), (3.0, o2), (10.0, o6), (7.0, o7), (5.0, o8)],
    elts = {o2, o3, o5, o6, o7, o8},

  • after heap.removeElementAt(...), before calling heapify(1)

    heap = [o1, (5.0, o8), (6.0, o3), (8.0, o5), (3.0, o2), (10.0, o6), (7.0, o7)],
    elts = {o2, o3, o5, o6, o7, o8},

  • at the end of heapify(1)

    heap = [o1, (5.0, o8), (6.0, o3), (8.0, o5), (3.0, o2), (10.0, o6), (7.0, o7)],
    elts = {o2, o3, o5, o6, o7, o8},

  • at the end of the whole method extractMin() which returns o4

    heap = [o1, (5.0, o8), (6.0, o3), (8.0, o5), (3.0, o2), (10.0, o6), (7.0, o7)],
    elts = {o2, o3, o5, o6, o7, o8},

Card Sets

The next activities are concerned with a class Hand, representing a set elements of Cards; recall that a set has no duplicates. Each Card c has c.rank which is a number (we treat Jack as 11, Queen as 12, King as 13 and Ace as 14) and c.suit which is a character (C for Clubs, D for Diamonds, H for Hearts, S for Spades). For simplicity we have a textual description of each object of type Card by a String such as "S12" the Queen of Spades, or "H6" for the six of Hearts.

• Consider the representation where a Hand is given concretely as a Vector suits and a Vector ranks. Each entry in suits is the character describing the suit of a card, and the corresponding (same index) entry of ranks is the int describing the rank of the same card. Thus if the concrete state is suits = ['D', 'C', 'D', 'S'], ranks = [6, 3, 12, 3] then the abstract state is the set {D6, C3, D12, S3}. Give a representation invariant and an abstraction function for this representation.
• Consider an alternative "bit-vector" representation, where the concrete state is bv, a 52-element long array of booleans. Each boolean records whether or not a particular card is present among the members of the Hand. We will use the order where the suits are ordered C, D, H, S, and within each suit the order is 2, 3,...10, Jack, Queen, King, Ace. To talk about this order, use the notation c.seqno. Thus the seqno of C2 is 1, of C3 is 2, of C4 is 3,..., of C13 is 12, of C14 is 13, of D2 is 14, of D3 is 15, ..., of D14 is 26, ... of S14 is 52. Thus bv[0] says whether the Hand contains C2; bv[12] says whether it contains C14, bv[13] says whether it contains D2, bv[25] says whether it contains D14, etc. That is, the abstraction function is
  • elements = {c | bv[c.seqno-1]=true}
  This representation has rep invariant "true"; every possible state of the array represents a valid Hand.

  Consider the method extractHighestRank(char c) which is specified abstractly by

       * @returns Card elt such that elt is in this.elements,
       *        && elt.suit==c
       *        && for all elt2 in this.elements, 
       *             if elt2.suit==c
       *             then elt.rank >= elt2.rank
       * @effects removes elt from this.elements and from the domain of priority
       * @throws NoSuchElementException if 
       *       for all elt2 in this.elements
       *           elt2.suit != c
  

  Write code to perform this method.