CMU MSE 15-671, Models of Software Systems, Fall 1995

Introduction to Z

Garlan & Wing Homework 6 Due: October 11, 1995

1. Write a Z specification of the following system. Your specification should include sufficient explanatory prose to make it easily readable.

A teacher wants to keep a register of students in the class, and to record which students have completed their homework. Specify:

A. The state space for a register. (Hint: use two sets of students.)

|---Register-----------------------
|	enrolled: P STUDENT
|	completed: P STUDENT
|-------
|	...
|--------------------------------

B. An operation to enroll a new student.

C. An operation to record that a student (already enrolled in class) has finished the homework.

D. An operation to enquire whether a student (who must be enrolled) has finished the homework. (The answer is either Yes or No).

E. A robust version of the system.

F. (Optional) A (robust) version of the system, assuming that, in addition, at most MAX students can be enrolled in the class. (You should not have to rewrite the whole specification to accomplish this.)

2. Write a Z specification of an answering machine.

A simple answering machine has two buttons "play" and "save", and can receive messages. If someone plays the messages and doesn't save them, they are erased/overwritten when the next message is received. The answering machine holds at most a specified number of messages; when it reaches full capacity, it refuses to accept new messages (and lights an error light).

Your state machine description should define a global variable MAXMSGS, which indicates the capacity of the answering machine. In addition to defining the state space for the machine, and its initial state, you should provide a description of operations to add a message; play the messages; and save the messages. Use the schema calculus to handle exceptional behavior, as we did with the Birthday Book.

3. The following questions refer to the class lecture on the Telephone Net.

A. Can a telephone Call itself? If so, what is the effect of a subsequent Busy operation?

B. Write an explicit Connect operation to connect a pair of phones.

C. Is it possible to place a call from a phone that's already busy?

D. Give an example that illustrates a situation in which a Hangup implies that a new connection will be made. Does the specification say which connection will be made if more than one is possible?

E. If a Hangup operations is applied to a ph? that is not yet connected, what happens? Briefly speculate on how the specification would have to be changed to make this more realistic.

F. Modify Busy so that it also indicates which phones ph? is connected to. What is the output if the input ph? is not connected at all?

G. Argue (informally -- at the level of the theorem proved in the lecture) that if a $Call$ request is made to connect two phones that are not already busy, then the connection will be made.