### LOGIC

Based on chapters 23 and 24 in The Way of Z.

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

 d1, d2: 1 .. 6

describes 36 possible combinations of values for d1 and d2

 d1 1 1 1 1 1 1 2 2 ... 6 6 d2 1 2 3 4 5 6 1 2 ... 5 6

This paragraph, with a stronger predicate,

 d1, d2: 1 .. 6 d1 + d2 = 7

describes only 6 possible combinations of values for d1 and d2

 d1 1 2 3 4 5 6 d2 6 5 4 3 2 1

THREE BASIC PREDICATES

There are three kinds of basic predicates.

Constants: true, false

Equations: e1 = e2

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 = { n1, n2, n3, ... },

 i: ns i nmax

means the same thing as

 n1 nmax n2 nmax n3 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 = { n1, n2, n3, ... },

 i: ns i nmax

means

 n1 nmax n2 nmax n3 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