### FORMAL REASONING

Based on chapter 15 in The Way of Z.

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.

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

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

 p true p Unit of and p false false Zero of and

 # 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

 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 ... design1 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