State Machine Models:
The Story So Far
•	Ways of describing state machines
>	graphically
>	as a 4-tuple 
(1) explicit enumeration 
(2) using predicates
>	as a special notation
(1) pre- & post-conditions 
(2) input, output, exceptions
•	Ways of reasoning about state machines
>	satisfaction of an invariant
>	reachability
The Next Five Lectures
•	New ways of describing state machines
>	Z global declarations
>	Z schemas
•	New ways of reasoning 
>	inferring derived properties of a state machine
>	calculating preconditions
>	adequacy of initial state
•	New ways of relating state machines
>	refinement/ implementation relationship
does what we specified
The Mathematics of Z
•	Typed set theory and logic
>	sets, relations, functions
>	first-order predicate logic
•	Schemas
>	“named” tuples -- like records
•	Schema calculus
>	mathematical operators for building bigger schemas out of smaller ones
•	Syntactic conventions 
>	to make descriptions tractable
>	to relate to programming
Schemas
•	The primary means of structuring formal specifications in Z is the use of schemas
•	Schemas describe
>	what states a system can occupy
>	what operations can happen
>	relationships between parts of a complex system
The Method of Z
•	Combine mathematics with prose
>	to explain the meaning of the symbols
>	to motivate the design decisions
•	Idioms for structuring large specifications
>	to make each part of the mathematics understandable
>	to reuse patterns of exposition and pieces of specification
•	Focus on abstract properties of a system
>	rather than algorithms, data structures, etc.
State Machines in Z
Global Variables
STATE := patients | field | setup | beam-on
VENT:= select_patient | select_field 
 enter | start | stop | ok | intlk

Example (continued)
Problems with this Approach
•	Ok for simple state machines, but ...
•	Global variables don’t scale
•	What about infinite state spaces?
•	What about parameters?
•	What about exceptions?
State Machines in Z
Schemas
A Simple Example
The State Space
BirthdayBook
Example
Observation 
•	There is:
>	No limit on the number of entries
>	No implied order of entries
>	No restriction on format
•	But there is a precise statement that:
>	Each person has only one birthday
>	Two people may share a birthday
>	Some people may not be in the database
Initial State
Operations
\
Add Birthday
Derived Components
The invariant
Reasoning About the Specification
Find Birthday
Remind
Summary
Error Handling
Successful Operations
Add Birthday- revised
Detecting Errors
Combining the Parts
The Other Operations
Advantages of Approach
Observation
Other Uses of the 
Schema Calculus
Summary
•	Z is a simple mathematical framework in which to:
>	describe systems abstractly yet precisely
>	compose a system out of small pieces
>	use old specifications to build new specifications
>	reason about properties of a system
>	relate views of a system

•	State invariant is assumed to hold across operations
>	so don't have to prove it is maintained
•	Operations applied outside of precondition lead to "chaos"
>	so always want final precondition to be "true"
•	Pre- and post-conditions are not distinguished syntactically
>	 but may be derived
•	Focus on state, not traces
•	Inputs, outputs, exceptions are simply notational conventions