LOGIC

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

Links to more Z lectures.

This page looks best when this \power and this X are about the same size: \power 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}
d1, d2: 1 .. 6
\end{axdef}

describes 36 possible combinations of values for d1 and d2

d1 11111122 ... 66
d2 12345612 ... 56

This paragraph, with a stronger predicate,

\begin{axdef}
d1, d2: 1 .. 6
\where
d1 + d2 = 7
\end{axdef}

describes only 6 possible combinations of values for d1 and d2

d1 123456
d2 654321

THREE BASIC PREDICATES

There are three kinds of basic predicates.

Constants: true, false

Equations: e1 = e2

Membership: x \in S

All predicates are built up from these.


SETS AND RELATIONS AS PREDICATES

Membership predicates (often with \in disguised):

odd(x) x \in (odd _)
5 < 12 5 \in (_ < _)
k divides 12 (k,12) \in divides
mother(ishmael, x) (ishmael,x) \in mother
leap year year \in (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.

\land     Conjunction, and (similar to && in C)
Used for combining requirements,
restriction, strengthening.
\lor Disjunction, or (similar to || in C)
Used for offering alternatives,
case analyses, weakening.
\lnot Negation, not (similar to ! in C)
\iff Equivalence, if and only if (== in C)
Used for definitions, ``equality''.
\implies Implication, if ... then ...
Used for conditional invariants, ordering.

CASE ANALYSES

Conjunction (\land, and) and disjunction (\lor, 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 (\implies, if) expresses ordering.

stronger predicate \implies related weaker predicate

p q p \implies 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.

\forall     Universal quantifer, all
Generalization of \land, and.
Used to describe sets (functions, ...),
bound variables range over set elements.
\exists Existential quantifer, some
Generalization of \lor, or.
Bound variables are ``hidden'' private data.

UNIVERSAL QUANTIFIER

The universal quantifer (\forall, all) generalizes and. Given free variable ns = { n1, n2, n3, ... },

\forall i: ns @ i \leq nmax

means the same thing as

n1 \leq nmax \land n2 \leq nmax \land n3 \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 (\exists, some) generalizes or. Given free variable ns = { n1, n2, n3, ... },

\exists i: ns @ i \leq nmax

means

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