Z lecture notes: Synthesis

SYNTHESIS

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

Sets (functions, relations, ...) and logic are all we need to write small formal descriptions.

Well-chosen notational conventions can make mathematical texts easier to read.

Formal descriptions are not just paraphrased natural language. Writing useful formal descriptions requires design judgment.

SET COMPREHENSION

Combine declaration, predicate, expression.

{ declaration | predicate

expression }

can be thought of this way

{ source | filter

pattern }

The expression and predicate are optional.

$\nat$ == { i: $\num$ | i $\geq$ 0 }

ODD == { i: $\num$

2*i+1 }

If the expression is the characteristic tuple, it can be omitted.

line == { x,y: $\num$ | y = m*x+b }

means the same as

line == { x,y: $\num$ | y = m*x+b

(x,y) }

SPECIFICATIONS

Set comprehensions are specifications in miniature.

A prime number is an integer larger than 1 that is only divisible by itself and 1. Informally,

PRIME == { 2, 3, 5, 7, 11, 13, 17, ... }

Paraphrasing the English

PRIME == { n: $\nat$ | n > 1 $\land$ $\lnot$ ( $\exists$ m: 2 .. n-1

n mod m = 0) }

Can't we do better? A prime is not a product of numbers larger than 1.

$\nat$ ₂ == $\nat$ \ { 0, 1 }

PRIME == $\nat$ ₂ \ { n,m: $\nat$ ₂

n * m }

We can make specifications clearer by moving away from a literal paraphrase of the English, and using set operators instead of negation and quantification.

LAMBDA EXPRESSION

Lambda expressions define functions.

( $\lambda$ declaration | predicate

expression)

isqr == ( $\lambda$ i: $\num$

i*i)

means the same as this set comprehension.

isqr == { i: $\num$

i $\mapsto$ i*i }

Both mean the same as

$\begin{axdef}$
		isqr: $\num$ $\fun$ $\nat$

	$\where$

		$\forall$ i: $\num$ isqr i = i*i
	$\end{axdef}$

Lambda expressions enable us to use functions without writing declarations.

9 = ( $\lambda$ i: $\num$

i*i) 3

RESTRICTED QUANTIFIERS

Restricted quantifiers abbreviate common predicates.

$\forall$ i: ns | odd(i)

i $\leq$ nmax

means

$\forall$ i: ns

odd(i) $\implies$ i $\leq$ nmax

and

$\exists$ i: ns | odd(i)

i $\leq$ nmax

means

$\exists$ i: ns

odd(i) $\land$ i $\leq$ nmax

In general

( $\forall$ d | p

q) $\iff$ ( $\forall$ d

p $\implies$ q)

( $\exists$ d | p

q) $\iff$ ( $\exists$ d

p $\land$ q)

CONVENIENCES AND SHORTCUTS

Local definitions factor out common expressions.

(let r == iroot(a)

r*r $\leq$ a < (r+1)*(r+1))

means

iroot(a) * iroot(a) $\leq$ a < (iroot(a)+1) * (iroot(a)+1)

Conditional expressions simplify two-way case analyses.

| x | = if x $\geq$ 0 then x else -x

means

(x $\geq$ 0 $\land$ | x | = x) $\lor$ (x < 0 $\land$ | x | = -x)

Back to Z lectures.

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