FORMAL REASONING

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


All properties do not have to be spelled out explicitly. From a few properties, we can infer many more by formal reasoning (applying rules).

Enables a formal model to act as a non-executable prototype.

Investigate behavior in hypothetical situations.

Validate a specification against requirements.

Check consistency and completeness.

Calculate preconditions.

Check refinement from specification to detailed design.


CALCULATION AND PROOF

An exercise in formal reasoning is a kind of calculation.

``A train moves at a constant velocity of sixty miles per hour. How far does the train travel in four hours?''

\begin{axdef}
distance, velocity, time: \nat
\where
distance = velocity * time
velocity = 60
time = 4
\end{axdef}

To find distance, substitute equals for equals. From a=b and b=c, conclude a=c.

distance = velocity * time Definition
    = 60 * time velocity = 60
    = 60 * 4 time = 4
    = 240 Arithmetic

The proof is a predicate in vertical format.


REASONING ABOUT SETS

Calculations need not be arithmetic.

``Philip works on the adhesives team in the materials group, which is part of the research division. Is Philip in research?''

\begin{axdef}
philip: PERSON
adhesives, materials, research,manufacturing: \power PERSON
\where
adhesives \subseteq materials
materials \subseteq research
philip \in adhesives
\end{axdef}

Show philip \in research.

philip \in adhesives   Definition
    \subseteq materials Definition
    \subseteq research Definition

Like equality, the subset relation is transitive. From S \subseteq T \subseteq U, infer S \subseteq U.


REASONING WITH EQUIVALENCE AND IMPLICATION

Each step can be a predicate, connected by the transitive logical connectives \iff and \implies.

\begin{axdef}
x: \num
\where
2*x + 7 = 13
\end{axdef}

Solve for x

2*x + 7 = 13 Definition
    \iff 2*x = 13 - 7 -7, both sides
    \iff 2*x = 6 Arithmetic
    \implies (2*x) div 2 = 6 div 2 div 2, both
    \iff x = 6 div 2 Algebra
    \iff x = 3 Arithmetic

We have proved 2*x + 7 = 13 \implies x = 3.


LAWS

Formal reasoning steps are justified by laws: predicates that are always true, for any values of the place holders.

Place holders can stand for expressions.

0 * n = 0 Zero
d \neq 0 \implies n = d*(n div d) + (n mod d)   Division
x=y \land x \in dom f \implies f x = f y Leibniz

Place holders can stand for predicates.

p \lor \lnot p Excluded middle
p \land \lnot p \iff false Contradiction
\lnot (p \land q) \iff \lnot p \lor \lnot q DeMorgan
p \land (q \lor r) \iff (p \land q) \lor (p \land r) Distrib.

SELECTED LAWS

About logical connectives

p \land true \iff p Unit of and
p \land false \iff false   Zero of and

About sequences

# \langle x \rangle = 1 Size of singleton
ran \langle x \rangle = { x } Range of singleton
# (s \cat t) = # s + #t # and \cat
ran (s \cat t) = ran s \cup ran t ran and \cat

About the existential quantifier

\exists d | p @ q \iff \exists d @ p \land q Restricted \exists
\exists x: T @ x = e \land p \iff p[e/x] 1-pt. rule

PRECONDITIONS BY INSPECTION

The precondition is the predicate that must be true for the operation to be defined, involving only inputs and unprimed ``before'' variables.

\begin{schema}{ Forward }

\Delta Editor
ch?: CHAR
\where
ch? = right_arrow
right \neq \langle \rangle
left' = left \cat \langle head(right) \rangle
right' = tail(right)
\end{schema}

The precondition is

ch? = right_arrow \land right \neq \langle \rangle

PRECONDITIONS BY INSPECTION (2)

A complete case analysis reduces to p \lor \lnot p

\begin{schema}{ T_Forward }

\Delta Editor
ch?: CHAR
\where
ch? = right_arrow
((right \neq \langle \rangle
    \land left' = left \cat \langle head right \rangle
    \land right' = tail right) \lor
(right = \langle \rangle \land left' = left \land right' = right))
\end{schema}

The precondition is

ch? = right_arrow \land
    ((right \neq \langle \rangle \land ...) \lor
    (right = \langle \rangle \land ...)) Given
    \iff ch? = right_arrow \land true   Excluded middle
    \iff ch? = right_arrow Unit of and

PRECONDITIONS BY CALCULATION

Implicit preconditions arise when the operation definition interacts with the state invariant.

The precondition of operation Op on state S is \exists S' @ Op, ``There exists a final state S' that satisfies the predicate of Op.''

\begin{schema}{ Insert }

\Delta Editor
ch?: CHAR
\where
ch? \in printing
left' = left \cat \langle ch? \rangle
right' = right
\end{schema}

The precondition of Insert is

\exists Editor' @ Insert

PRECONDITION CALCULATION

\exists Editor' @ Insert

\iff \exists left', right': TEXT |
    # (left' \cat right') \leq maxsize @
    ch? \in printing \land
    left' = left \cat \langle ch? \rangle \land right' = right Expand schemas
\iff \exists left', right': TEXT @
    # (left' \cat right') \leq maxsize \land pr \land ... \exists, pr is ch? \in printing
\iff pr \land # ((left \cat \langle ch? \rangle) \cat right) \leq maxsize   1-pt. rule w/ left',right'
\iff pr \land # left + # \langle ch? \rangle + # right \leq maxsize # and \cat
\iff pr \land # left + 1 + # right \leq maxsize Size of singleton
\iff pr \land # left + # right < maxsize Arithmetic

The precondition is

ch? \in printing \land # left + # right < maxsize

The buffer mustn't overflow!


REFINEMENT, IMPLEMENTATION

Implication can be used to check the correctness of design steps (refinement steps).

p \implies q means p has all the properties of q, and possibly more besides. If you asked for q, you should be satisfied with p.

stronger \implies weaker
concrete \implies abstract
implementation \implies specification
impl. \implies design_n \implies ... \implies design1 \implies spec.

Example

x' > x Specification
x' = x+1 Implementation
x' = x+1 \implies x' > x Proof

Back to Z lectures.


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