Homework IX
Note that the chapter by Guttag, Horowitz and Musser is silent about the treatment of exceptions. In fairness, it should be recognized that this was early work, written before the techniques for treating errors discussed in class were developed (see the chapter by Goguen, Thatcher and Wagner for a discussion of the OK-function strategy, and chapter 7 of von Horebeek for an alternative).
(a) [10 points]
In the absence of any comment in Guttag et al about exceptions, we could reasonably apply the "errors propagate" assumption to their specifications. Given the "errors propagate" assumption (and regarding their 'UNDEFINED' as an error), show that their CircularList specification (Figure 4.2.2, page 64) is inconsistent. Note that this specification has a typo -- the right side of equation 17 should read INSERT(RIGHT(INSERT(c,i1)),i).
(b) [40 points]
Correct the Guttag et al CircularList specification and argue that your corrected version is a consistent and sufficiently complete specification of circular lists
Given Guttag's CircularList equations (Figure 4.2.2) and the QREP equations (Figure 4.3.1), prove that the Queue equation (Figure 4.2.3)
11. DELETEQ(ADDQ(q,i)) =
12. if ISNEWQ(q) then NEWQ
13. else ADDQ(DELETEQ(q),i)
must be valid.