Based on chapters 23 and 24 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.

Logic can be used for description or for proof.

Z emphasizes the descriptive use of logic.

Formulas in logic are called predicates. Predicates evaluate to one of the two truth values true and false.

When used for description, logic classifies situations into two categories: acceptable (predicate evaluates to true) and unacceptable (false).

A Z specification describes all of the situations where all of its predicates are true.

Used in this way, predicates act as acceptance tests.


Predicates can act as acceptance tests.

We make predicates stronger by adding restrictions that eliminate candidate objects, resulting in fewer acceptable objects that are more specialized.

This paragraph

d1, d2: 1 .. 6

describes 36 possible combinations of values for d1 and d2

d1 11111122 ... 66
d2 12345612 ... 56

This paragraph, with a stronger predicate,

d1, d2: 1 .. 6
d1 + d2 = 7

describes only 6 possible combinations of values for d1 and d2

d1 123456
d2 654321


There are three kinds of basic predicates.

Constants: true, false

Equations: e1 = e2

Membership: x \in S

All predicates are built up from these.


Membership predicates (often with \in disguised):

odd(x) x \in (odd _)
5 < 12 5 \in (_ < _)
k divides 12 (k,12) \in divides
mother(ishmael, x) (ishmael,x) \in mother
leap year year \in (leap _)

To use prefix syntax, declare with underscore.

odd _, ODD: \power \num

k \in ODD

To use infix syntax, just apply underlining.

divides: \num \rel \num

(k,12) \in divides
k divides 12


Build up complex predicates from basic ones.

\land     Conjunction, and (similar to && in C)
Used for combining requirements,
restriction, strengthening.
\lor Disjunction, or (similar to || in C)
Used for offering alternatives,
case analyses, weakening.
\lnot Negation, not (similar to ! in C)
\iff Equivalence, if and only if (== in C)
Used for definitions, ``equality''.
\implies Implication, if ... then ...
Used for conditional invariants, ordering.


Conjunction (\land, and) and disjunction (\lor, or) work together to express case analyses.

Conjunction combines the conditions that are found together in the same case; disjunction separates the cases.

TEMP == \num
PHASE ::= solid | liquid | gas

temp: TEMP
phase: PHASE
(temp < 0 \land phase = solid) \lor
(0 \leq temp \leq 100 \land phase = liquid) \lor
(temp > 100 \land phase = gas)

This is a very common pattern in Z.


Implication (\implies, if) expresses ordering.

stronger predicate \implies related weaker predicate

p q p \implies q
false false true
false true true
true false false
true true true

It can express conditional safety requirements.

BEAM ::= off | on
DOOR ::= closed | open

beam: BEAM
door: DOOR
beam = on \implies door = closed

This Z describes three situations involving the beam and the door.

BEAM off off on
DOOR closed open closed


Quantifiers introduce local (``bound'') variables into predicates so they can describe indefinitely large collections of objects.

\forall     Universal quantifer, all
Generalization of \land, and.
Used to describe sets (functions, ...),
bound variables range over set elements.
\exists Existential quantifer, some
Generalization of \lor, or.
Bound variables are ``hidden'' private data.


The universal quantifer (\forall, all) generalizes and. Given free variable ns = { n1, n2, n3, ... },

\forall i: ns @ i \leq nmax

means the same thing as

n1 \leq nmax \land n2 \leq nmax \land n3 \leq nmax \land ...

The universal quantifier enables a single predicate to describe (define) an entire set (relation, function, sequence, ...). Bound variables range over set elements and can act as place holders in definitions.

divides: \num \rel \num
\forall d,n: \num @ d divides n \iff n mod d = 0


The existential quantifer (\exists, some) generalizes or. Given free variable ns = { n1, n2, n3, ... },

\exists i: ns @ i \leq nmax


n1 \leq nmax \lor n2 \leq nmax \lor n3 \leq nmax \lor ...

The existential quantifier enables definitions to use private, ``hidden'' variables which may be constrained to particular values.

_ mod _ : \num \fun (\num \ { 0 }) \fun \num
\forall n,r: \num; q: \num \ { 0 } @
    n mod q = r \iff (\exists d @ r < d \land n = q*d + r)

Back to Z lectures.

Jonathan Jacky / University of Washington / Seattle, Washington / USA
E-mail: jon@u.washington.edu