Based on chapter 8 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.

Three basic constructs:

Declarations introduce variables.

Expressions describe values that variables can assume.

Predicates place constraints on the values that variables do assume.


Set display

{ 1, 2, 3, 4, 5, 6 }
{ 4, 5, 6, 1, 2, 3 }
{ 4, 5, 5, 6, 1, 1, 1, 2, 3 }
{ red, yellow, green }
{ yellow, red, green, 1, 2 }     Type error!

Set names


Set expressions

1 .. 6
{  i: \num | 1 \leq i \leq 6  }


Every object belongs to a set called its type.

1, 2, ... all belong to the type \num.

red, green belong to the type COLOR.

Every type must be introduced in a declaration. There are two ways to declare types.

Free types are like enumerations.

COLOR ::= red | green | blue | yellow
    | cyan | magenta | white | black

Basic types can include indefinitely many elements.



A variable is a name for an object: its value. Variables are introduced in declarations.

x: S     The value of x belongs to set S

Axiomatic definitions declare global variables and can include optional constraints.

d1,d2: DICE
d1 + d2 = 7
d1 < d2

Constants are variables that are constrained to one value (\power S means set of S).

DICE: \power \num
DICE = 1 .. 6

Abbreviation definitions can also declare constants.

DICE == 1 .. 6


Types are sets, but not all sets are types.

ODD, EVEN, PRIME are just sets, \num is their type.

Any set can appear in a declaration.

o: ODD

In a normalized declaration, we write the signature to show the type.

e,o,p: \num
e \in EVEN
o \in ODD
p \in PRIME

The type determines which variables can be combined in expressions.


Expressions have values. The simplest expressions are constants and variables.

1, 2, red, x, d1, DICE, \num, ...

Operators build larger expressions from smaller ones. Arithmetic provides familiar examples.

m+n   Addition
m-n   Subtraction
m*n   Multiplication
m div n   Division
m mod n   Remainder (modulus)
m \leq n   Less than or equal
m .. n   Number range (up to)
min A   Minimum of a set of numbers
max A   Maximum of a set of numbers


The size operator # counts elements.

# { red, yellow, blue, green, red } = 4

The union operator \cup combines sets.

{ 1, 2, 3 } \cup { 2, 3, 4 } = { 1, 2, 3, 4 }

The difference operator \ removes the elements of one set from another.

{ 1, 2, 3, 4 } \ { 2, 3 } = { 1, 4 }

The intersection operator \cap finds the elements common to both sets.

{ 1, 2, 3 } \cap { 2, 3, 4 } = { 2, 3 }

Set operators work with sets of any type, but

{ 1, 2, 3 } \cup { red, green }     Type error!


Predicates constrain values. Many have the form e1 R e2, where e1 and e2 are expressions.

Equality, x and y have the same value.

x = y

Arithmetic relations, n is less than m.

n < m

Set membership, x is a member of S.

x \in S

Subset, members of S are members of T.

S \subseteq T

Predicates are not expressions. They do not have values, they are true or false.


A train moves at a constant velocity of sixty miles per hour for four hours.

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

How far does the train travel?

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

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

Is Philip in the research division?


1. Compare this Z

DICE == 1 .. 6

d1,d2: DICE
d1 + d2 = 7
d1 < d2

with this C.

    typedef int DICE;
    DICE d1, d2;

2. Compare this basic type and definition


x,y: X

with this free type.

X ::= x | y

Back to Z lectures.

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