This Lecture
•	Establishing properties about a model
>	Properties of the state space 
»	e.g., initial state space is not empty
>	Properties of operations 
»	values of unspecified variables
»	preconditions of operations
•	Relating models: refinement
>	State
»	Abstraction relations
»	Initial states property
>	Operations
»	Applicability
»	Correctness
You Should Know
•	How to state the Initialization Theorem.
•	How to apply the 1-point rule.
•	How to write down the formula for calculating the pre-condition of an operation.
•	How to write down an abstraction relation as a schema.
•	What refinement means
>	whether one relation refines another
>	what you need to prove for schemas
Informal versus Formal Reasoning
Formal Proofs using Z
Schemas as Hypotheses
Schemas as Hypotheses (cont)

Schemas as Conclusions
Example
The Initialization Theorem
Example
Example (cont)
The One-Point Rule
Two Useful Identities
1.  " x: T | P(x) ∑ Q(x) 
∫ 
  " x: T ∑ P(x) ﬁ Q(x)

2.  $ x: T | P(x) ∑ Q(x) 
∫ 
  $ x: T ∑ P(x) Ÿ Q(x)

Example
Precondition Calculation
Example
Preconditions (cont)
Example
Example (cont)
General Reasoning
Implementation/Refinement
•	Qn: Given two state machines, what does it mean to say one implements another?
•	Ans: The second machine should do at least what the first machine does.
•	Note: It can do more, and if the abstract machine leaves some options open, then it can chose one of those options.
Methods of Refinement in Z

Observations
Recall

Data Refinement in Z
Abstraction Function
The Initial States Theorem

Operation Refinement
Relations
Schemas
General Case
Example

Applicability (informal)
Correctness (informal)