Z lecture notes: Logic

LOGIC

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

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.

USING PREDICATES FOR DESCRIPTION.

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

$\begin{axdef}$
		d₁, d₂: 1 .. 6
	$\end{axdef}$

describes 36 possible combinations of values for d₁ and d₂

`d₁`	1	1	1	1	1	1	2	2	...	6	6
`d₂`	1	2	3	4	5	6	1	2	...	5	6

This paragraph, with a stronger predicate,

$\begin{axdef}$
		d₁, d₂: 1 .. 6

	$\where$

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

describes only 6 possible combinations of values for d₁ and d₂

`d₁`	1	2	3	4	5	6
`d₂`	6	5	4	3	2	1

THREE BASIC PREDICATES

There are three kinds of basic predicates.

Constants: true, false

Equations: e₁ = e₂

Membership: x S

All predicates are built up from these.

SETS AND RELATIONS AS PREDICATES

Membership predicates (often with disguised):

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

To use prefix syntax, declare with underscore.

$\begin{axdef}$
		odd _, ODD: $\power$ $\num$
	$\end{axdef}$

odd(k)

k $\in$ ODD

To use infix syntax, just apply underlining.

$\begin{axdef}$
		divides: $\num$ $\rel$ $\num$
	$\end{axdef}$

(k,12) $\in$ divides

k divides 12

LOGICAL CONNECTIVES

Build up complex predicates from basic ones.

	Conjunction, and (similar to `&&` in C)
	Used for combining requirements,
	restriction, strengthening.

	Disjunction, or (similar to `\|\|` in C)
	Used for offering alternatives,
	case analyses, weakening.

	Negation, not (similar to `!` in C)

	Equivalence, if and only if (`==` in C)
	Used for definitions, ``equality''.

	Implication, if ... then ...
	Used for conditional invariants, ordering.

CASE ANALYSES

Conjunction (, and) and disjunction (, 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

$\begin{axdef}$
		temp: TEMP
		phase: PHASE

	$\where$

		(temp < 0 $\land$ phase = solid) $\lor$
		(0 $\leq$ temp $\leq$ 100 $\land$ phase = liquid) $\lor$
		(temp > 100 $\land$ phase = gas)
	$\end{axdef}$

This is a very common pattern in Z.

IMPLICATION

Implication (, if) expresses ordering.

stronger predicate $\implies$ related weaker predicate

`p`	`q`	`p 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

$\begin{axdef}$
		beam: BEAM
		door: DOOR

	$\where$

		beam = on $\implies$ door = closed
	$\end{axdef}$

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

`BEAM`	`off`	`off`	`on`
`DOOR`	`closed`	`open`	`closed`

QUANTIFIERS

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

	Universal quantifer, all
	Generalization of , and.
	Used to describe sets (functions, ...),
	bound variables range over set elements.

	Existential quantifer, some
	Generalization of , or.
	Bound variables are ``hidden'' private data.

UNIVERSAL QUANTIFIER

The universal quantifer (, all) generalizes and. Given free variable ns = { n₁, n₂, n₃, ... },

$\forall$ i: ns

i $\leq$ nmax

means the same thing as

n₁ $\leq$ nmax $\land$ n₂ $\leq$ nmax $\land$ n₃ $\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.

$\begin{axdef}$
		divides: $\num$ $\rel$ $\num$

	$\where$

		$\forall$ d,n: $\num$ d divides n $\iff$ n mod d = 0
	$\end{axdef}$

EXISTENTIAL QUANTIFIER

The existential quantifer (, some) generalizes or. Given free variable ns = { n₁, n₂, n₃, ... },

$\exists$ i: ns

i $\leq$ nmax

means

n₁ $\leq$ nmax $\lor$ n₂ $\leq$ nmax $\lor$ n₃ $\leq$ nmax $\lor$ ...

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

$\begin{axdef}$
		_ mod _ : $\num$ $\fun$ ( $\num$ \ { 0 }) $\fun$ $\num$

	$\where$

		$\forall$ n,r: $\num$ ; q: $\num$ \ { 0 }
		n mod q = r $\iff$ ( $\exists$ d r < d $\land$ n = q*d + r)
	$\end{axdef}$

Back to Z lectures.

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