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

d_{1}, d_{2}: 1 .. 6 | ||

describes 36 possible combinations of values for
`d _{1}` and

d _{1} |
1 | 1 | 1 | 1 | 1 | 1 | 2 | 2 | ... | 6 | 6 |

d _{2} |
1 | 2 | 3 | 4 | 5 | 6 | 1 | 2 | ... | 5 | 6 |

This paragraph, with a stronger predicate,

d_{1}, d_{2}: 1 .. 6 | ||

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

describes only 6 possible combinations of values for
`d _{1}` and

d _{1} |
1 | 2 | 3 | 4 | 5 | 6 |

d _{2} |
6 | 5 | 4 | 3 | 2 | 1 |

THREE BASIC PREDICATES

There are three kinds of basic predicates.

*Constants*: `true`, `false`

*Equations*: `e _{1} = e_{2}`

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

odd _, ODD: | ||

odd(k) |

k ODD |

To use *infix* syntax, just apply *underlining*.

divides: | ||

(k,12) 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 == |

PHASE ::= solid | liquid | gas |

temp: TEMP | ||

phase: PHASE | ||

(temp < 0 phase = solid) | ||

(0 temp 100 phase = liquid) | ||

(temp > 100 phase = gas) | ||

This is a very common pattern in Z.

IMPLICATION

Implication (`, `*if*) expresses *ordering*.

stronger predicate 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 |

beam: BEAM | ||

door: DOOR | ||

beam = on door = closed | ||

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 _{1}, n_{2}, n_{3}, ... }`,

i: ns i nmax |

means the same thing as

n_{1} nmax n_{2} nmax n_{3} nmax ... |

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.

divides: | ||

d,n: d divides n n mod d = 0 | ||

EXISTENTIAL QUANTIFIER

The *existential quantifer* (`, `*some*) generalizes *or*. Given *free variable* `ns = { n _{1}, n_{2}, n_{3}, ... }`,

i: ns i nmax |

means

n_{1} nmax n_{2} nmax n_{3} nmax ... |

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

_ mod _ : ( \ { 0 }) | ||

n,r: ; q: \ { 0 } | ||

n mod q = r ( d r < d n = q*d + r) | ||

Back to Z lectures.

Jonathan Jacky / University of Washington / Seattle, Washington / USA

E-mail: jon@u.washington.edu