Homework #1 (Part II): CSE503, Winter 2002

1. (25 points) Take the algebraic specification of a queue sketched in lecture as a basis.  Extend (and modify if necessary) the specification to more accurately reflect common understandings of queues.  You are required to handle the issue of queues that become full as part of the specification.
2. (25 points) Take the PhoneDB schemas sketched in lecture as a basis.  Extend (and modify if necessary) the specification to handle (a) the addition of new members, (b) a lookup schema that reports members associated with a given phone number, (c) error detection and reporting in a consistent manner, and (d) initialization of the schema.   In addition, for (a) show that the proof obligations of PhoneDB are satisfied.
3. (25 points) Write a statechart-style specification for some device you can find on campus.  Choices include: the operator console in one of the EE1 classrooms, the microwave oven on the fourth floor of Sieg Hall, etc.  You may use an appropriate level of abstraction (as opposed to modeling the device in complete detail).