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

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?''

distance, velocity, time: | ||

distance = velocity * time | ||

velocity = 60 | ||

time = 4 | ||

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?''

philip: PERSON | ||

adhesives, materials, research,manufacturing: PERSON | ||

adhesives materials | ||

materials research | ||

philip adhesives | ||

Show `philip research`.

philip adhesives | Definition |

materials | Definition |

research | Definition |

Like equality, the subset relation is *transitive*.
From `S T U`, infer
`S U`.

REASONING WITH EQUIVALENCE AND IMPLICATION

Each step can be a predicate, connected by
the transitive logical connectives ` and ``.
`

x: | ||

2*x + 7 = 13 | ||

Solve for `x`

2*x + 7 = 13 | Definition |

2*x = 13 - 7 | -7, both sides |

2*x = 6 | Arithmetic |

(2*x) div 2 = 6 div 2 | , both div 2 |

x = 6 div 2 | Algebra |

x = 3 | Arithmetic |

We have proved `2*x + 7 = 13 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 0 n = d*(n div d) + (n mod d) | Division |

x=y x dom f f x = f y | Leibniz |

Place holders can stand for predicates.

p p | Excluded middle |

p p false | Contradiction |

(p q) p q | DeMorgan |

p (q r) (p q) (p r) | Distrib. |

SELECTED LAWS

About logical connectives

p true p | Unit of and |

p false false | Zero of and |

About sequences

# x = 1 | Size of singleton |

ran x = { x } | Range of singleton |

# (s t) = # s + #t | # and |

ran (s t) = ran s ran t | and ran |

About the existential quantifier

d | p q d p q | Restricted |

x: T x = e p 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.

Forward | |||

Editor | |||

ch?: CHAR | |||

ch? = right_arrow | |||

right | |||

left' = left head(right) | |||

right' = tail(right) | |||

The precondition is

ch? = right_arrow right |

PRECONDITIONS BY INSPECTION (2)

A complete case analysis reduces to `p p`

T_Forward | |||

Editor | |||

ch?: CHAR | |||

ch? = right_arrow | |||

((right | |||

left' = left head right | |||

right' = tail right) | |||

(right = left' = left right' = right)) | |||

The precondition is

ch? = right_arrow | |

((right ...) | |

(right = ...)) | Given |

ch? = right_arrow true | Excluded middle |

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 ` S' Op`,
``There exists a final state `S'` that satisfies the
predicate of `Op`.''

Insert | |||

Editor | |||

ch?: CHAR | |||

ch? printing | |||

left' = left ch? | |||

right' = right | |||

The precondition of `Insert` is

Editor' Insert |

PRECONDITION CALCULATION

` Editor' Insert`

left', right': TEXT | | |

# (left' right') maxsize | |

ch? printing | |

left' = left ch? right' = right | Expand schemas |

left', right': TEXT | |

# (left' right') maxsize pr ... | , pr is ch? printing |

pr # ((left ch? ) right) maxsize | 1-pt. rule w/ left',right' |

pr # left + # ch? + # right maxsize | # and |

pr # left + 1 + # right maxsize | Size of singleton |

pr # left + # right < maxsize | Arithmetic |

The precondition is

ch? printing # left + # right < maxsize |

The buffer mustn't overflow!

REFINEMENT, IMPLEMENTATION

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

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

concrete abstract |

implementation specification |

impl. design_n ... design_{1} spec. |

Example

x' > x | Specification |

x' = x+1 | Implementation |

x' = x+1 x' > x | Proof |

Back to Z lectures.

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

E-mail: jon@u.washington.edu