The Story Thus Far
•	We have seen a brief intro to Z
•	Main features
>	use of schemas to encapsulate state
>	use of schemas to describe operations
>	the delta and xi conventions
>	use of schema calculus to build up bigger operations out of smaller ones
Relating Birthday Book 
to State Machines
S = {known: NAME; birthday: NAME  £  DATE |
known = dom(birthday)}
I = {known: NAME; birthday: NAME  £  DATE |
birthday = ∆}
A = {AddBirthday(date?:DATE, name?:NAME),
FindBirthday(date?:DATE)/name!(NAME),
Remind(date?:DATE)/names!(P Name)}
d = ...

AddBirthday
AddBirthday(date?:DATE, name?:NAME)
pre name? œ  known
post birthday' = birthday » { name? ¢ date? }

FindBirthday(date?:DATE)/name!(NAME)
pre name? ⁄ known
post birthday' = birthday
known’ = known
name! = birthday(date?)
RAddBirthday
RAddBirthday(date?:DATE, name?:NAME) 					report!(REPORT)
pre true
post 
(name? œ  known ﬂ 
birthday' = birthday » { name? ¢ date? } ﬂ 
report = ok)
‡ 
(name? ⁄ known ﬂ 
birthday' = birthday ﬂ 
known’= knownﬂ
report = alreadyknown)
  
Lecture Outline
•	A Second Example: Telephone Net
>	Adapted from "Telephone Network", by Carroll Morgan
>	In Specification Case Studies, Ian Hayes (ed)
•	Concepts
>	Use of strong state invariants to make concise models
>	Use of schema calculus to simplify descriptions and associated reasoning
>	Disj, (Generic Definitions) 
>	Framing
>	Reasoning with state invariants
Telephones
Requests for Connection
Connections
Operations
•	Call: Request a connection between two phones
•	Hangup: Terminate a connection
•	Busy: Report whether a phone is busy
State Space
Example
Pairwise disjoint sets
What's Wrong With This Net?
An Inefficient Net
Efficient Networks

Initial Telephone Net
Framing: Event
This Really Means ...
Call
Example
Example
Hangup
Busy
Reasoning about the Specification
•	Theorem: (Informal) If an operation doesn't change any of the requests then it doesn't change any of the connections.
•	Proof: (Informal)
1. The constraint on Event tells us that any original connection won't be broken if it is still requested.
2. If an operation doesn't change the requests, all original connections will still be requested.
3. Hence, no connections are broken.
4. Also, no new connections are added because if a connection could be added afterwards, it could have been added before.
5. So connections aren't changed.
The Fuzz Type Checker 
•	One of the benefits of being precise about types is that we can type-check our descriptions
•	We will use the Fuzz Type Checker to do this.
•	It takes Latex descriptions of Z specifications as input and produces error reports and other useful type information.
•	To type check a file spec.tex, invoke
fuzz spec.tex
•	To get type information about spec.tex, invoke
fuzz -t spec.tex
Last Slide