Z lecture notes: Formal Reasoning

FORMAL REASONING

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

$\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 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 .

$\begin{axdef}$
		x: $\num$

	$\where$

		2*x + 7 = 13
	$\end{axdef}$

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`	`div 2`, both
`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`	`ran` and

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.

$\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 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`
`((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.''

$\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

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? $\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 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$ design₁ $\implies$ 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