Based on chapter 8 in The Way of Z.

Links to more Z lectures.

This page looks best when this ` and this ``X` are
about the same size: ` 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.

SETS

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

| |

DICE | |

LAMP |

Set expressions

1 .. 6 | |

{ i: | 1 i 6 } |

TYPES

Every object belongs to a set called its *type*.

`1`, `2`, `...` all belong to the type `.
`

`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.

| |

[NAME] | |

[PROCESS, FILE] |

VARIABLES

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*.

d_{1},d_{2}: DICE | ||

d_{1} + d_{2} = 7 | ||

d_{1} < d_{2} | ||

*Constants* are variables that are constrained to one value
(` S` means *set of S*).

DICE: | ||

DICE = 1 .. 6 | ||

*Abbreviation definitions* can also declare
constants.

DICE == 1 .. 6 |

TYPES, SETS AND NORMALIZATION

Types are sets, but not all sets are types.

`ODD, EVEN, PRIME` are just sets, ` is their type.
`

Any set can appear in a declaration.

e: EVEN | ||

o: ODD | ||

p: PRIME | ||

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

e,o,p: | ||

e EVEN | ||

o ODD | ||

p PRIME | ||

The type determines which variables can be combined in expressions.

EXPRESSIONS AND OPERATORS, ARITHMETIC

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

1, 2, red, x, d, _{1}DICE, , ... |

*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 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 |

SET OPERATORS

The *size* operator `#` counts elements.

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

The *union* operator ` combines sets.
`

{ 1, 2, 3 } { 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 ` finds the elements common to
both sets.
`

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

Set operators work with sets of any type, but

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

PREDICATES

Predicates *constrain* values. Many
have the form `e _{1} R e_{2}`, where

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 S |

Subset, members of `S` are members of `T`.

S T |

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

PUTTING THE ELEMENTS TOGETHER

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

distance, velocity, time: | ||

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: PERSON | ||

adhesives materials | ||

materials research | ||

philip adhesives | ||

Is Philip in the research division?

ELEMENTS OF Z: DISCUSSION

1. Compare this Z

DICE == 1 .. 6 |

d_{1},d_{2}: DICE | ||

d_{1} + d_{2} = 7 | ||

d_{1} < d_{2} | ||

with this C.

`typedef int DICE;`

`DICE d1, d2;`

[X] |

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