Based on chapter 15 in The Way of Z.

Links to more Z lectures.

This page looks best when this \power and this X are about the same size: \power X. See these viewing tips.

All properties do not have to be spelled out explicitly. From a few properties, we can infer many more by formal reasoning (applying rules).

Enables a formal model to act as a non-executable prototype.

Investigate behavior in hypothetical situations.

Validate a specification against requirements.

Check consistency and completeness.

Calculate preconditions.

Check refinement from specification to detailed design.


An exercise in formal reasoning is a kind of calculation.

``A train moves at a constant velocity of sixty miles per hour. How far does the train travel in four hours?''

distance, velocity, time: \nat
distance = velocity * time
velocity = 60
time = 4

To find distance, substitute equals for equals. From a=b and b=c, conclude a=c.

distance = velocity * time Definition
    = 60 * time velocity = 60
    = 60 * 4 time = 4
    = 240 Arithmetic

The proof is a predicate in vertical format.


Calculations need not be arithmetic.

``Philip works on the adhesives team in the materials group, which is part of the research division. Is Philip in research?''

philip: PERSON
adhesives, materials, research,manufacturing: \power PERSON
adhesives \subseteq materials
materials \subseteq research
philip \in adhesives

Show philip \in research.

philip \in adhesives   Definition
    \subseteq materials Definition
    \subseteq research Definition

Like equality, the subset relation is transitive. From S \subseteq T \subseteq U, infer S \subseteq U.


Each step can be a predicate, connected by the transitive logical connectives \iff and \implies.

x: \num
2*x + 7 = 13

Solve for x

2*x + 7 = 13 Definition
    \iff 2*x = 13 - 7 -7, both sides
    \iff 2*x = 6 Arithmetic
    \implies (2*x) div 2 = 6 div 2 div 2, both
    \iff x = 6 div 2 Algebra
    \iff x = 3 Arithmetic

We have proved 2*x + 7 = 13 \implies x = 3.


Formal reasoning steps are justified by laws: predicates that are always true, for any values of the place holders.

Place holders can stand for expressions.

0 * n = 0 Zero
d \neq 0 \implies n = d*(n div d) + (n mod d)   Division
x=y \land x \in dom f \implies f x = f y Leibniz

Place holders can stand for predicates.

p \lor \lnot p Excluded middle
p \land \lnot p \iff false Contradiction
\lnot (p \land q) \iff \lnot p \lor \lnot q DeMorgan
p \land (q \lor r) \iff (p \land q) \lor (p \land r) Distrib.


About logical connectives

p \land true \iff p Unit of and
p \land false \iff false   Zero of and

About sequences

# \langle x \rangle = 1 Size of singleton
ran \langle x \rangle = { x } Range of singleton
# (s \cat t) = # s + #t # and \cat
ran (s \cat t) = ran s \cup ran t ran and \cat

About the existential quantifier

\exists d | p @ q \iff \exists d @ p \land q Restricted \exists
\exists x: T @ x = e \land p \iff p[e/x] 1-pt. rule


The precondition is the predicate that must be true for the operation to be defined, involving only inputs and unprimed ``before'' variables.

\begin{schema}{ Forward }

\Delta Editor
ch?: CHAR
ch? = right_arrow
right \neq \langle \rangle
left' = left \cat \langle head(right) \rangle
right' = tail(right)

The precondition is

ch? = right_arrow \land right \neq \langle \rangle


A complete case analysis reduces to p \lor \lnot p

\begin{schema}{ T_Forward }

\Delta Editor
ch?: CHAR
ch? = right_arrow
((right \neq \langle \rangle
    \land left' = left \cat \langle head right \rangle
    \land right' = tail right) \lor
(right = \langle \rangle \land left' = left \land right' = right))

The precondition is

ch? = right_arrow \land
    ((right \neq \langle \rangle \land ...) \lor
    (right = \langle \rangle \land ...)) Given
    \iff ch? = right_arrow \land true   Excluded middle
    \iff ch? = right_arrow Unit of and


Implicit preconditions arise when the operation definition interacts with the state invariant.

The precondition of operation Op on state S is \exists S' @ Op, ``There exists a final state S' that satisfies the predicate of Op.''

\begin{schema}{ Insert }

\Delta Editor
ch?: CHAR
ch? \in printing
left' = left \cat \langle ch? \rangle
right' = right

The precondition of Insert is

\exists Editor' @ Insert


\exists Editor' @ Insert

\iff \exists left', right': TEXT |
    # (left' \cat right') \leq maxsize @
    ch? \in printing \land
    left' = left \cat \langle ch? \rangle \land right' = right Expand schemas
\iff \exists left', right': TEXT @
    # (left' \cat right') \leq maxsize \land pr \land ... \exists, pr is ch? \in printing
\iff pr \land # ((left \cat \langle ch? \rangle) \cat right) \leq maxsize   1-pt. rule w/ left',right'
\iff pr \land # left + # \langle ch? \rangle + # right \leq maxsize # and \cat
\iff pr \land # left + 1 + # right \leq maxsize Size of singleton
\iff pr \land # left + # right < maxsize Arithmetic

The precondition is

ch? \in printing \land # left + # right < maxsize

The buffer mustn't overflow!


Implication can be used to check the correctness of design steps (refinement steps).

p \implies q means p has all the properties of q, and possibly more besides. If you asked for q, you should be satisfied with p.

stronger \implies weaker
concrete \implies abstract
implementation \implies specification
impl. \implies design_n \implies ... \implies design1 \implies spec.


x' > x Specification
x' = x+1 Implementation
x' = x+1 \implies x' > x Proof

Back to Z lectures.

Jonathan Jacky / University of Washington / Seattle, Washington / USA