Z lecture notes: Elements

ELEMENTS OF Z

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.

$\begin{axdef}$
		d₁,d₂: DICE

	$\where$

		d₁ + d₂ = 7
		d₁ < d₂
	$\end{axdef}$

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

$\begin{axdef}$
		DICE: $\power$ $\num$

	$\where$

		DICE = 1 .. 6
	$\end{axdef}$

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.

$\begin{axdef}$
		e: EVEN
		o: ODD
		p: PRIME
	$\end{axdef}$

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

$\begin{axdef}$
		e,o,p: $\num$

	$\where$

		e $\in$ EVEN
		o $\in$ ODD
		p $\in$ PRIME
	$\end{axdef}$

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₁, 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 } $\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 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

Predicates constrain values. Many have the form e₁ R e₂, where e₁ and e₂ 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.

PUTTING THE ELEMENTS TOGETHER

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

$\begin{axdef}$
		distance, velocity, time: $\nat$

	$\where$

		distance = velocity * time
		velocity = 60
		time = 4
	$\end{axdef}$

How far does the train travel?

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

$\begin{axdef}$
		philip: PERSON
		adhesives, materials, research,
		manufacturing: $\power$ PERSON

	$\where$

		adhesives $\subseteq$ materials
		materials $\subseteq$ research
		philip $\in$ adhesives
	$\end{axdef}$

Is Philip in the research division?

ELEMENTS OF Z: DISCUSSION

1. Compare this Z

DICE == 1 .. 6

$\begin{axdef}$
		d₁,d₂: DICE

	$\where$

		d₁ + d₂ = 7
		d₁ < d₂
	$\end{axdef}$

with this C.

typedef int DICE;
DICE d1, d2;

2. Compare this basic type and definition

[X]

$\begin{axdef}$
		x,y: X
	$\end{axdef}$

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