Based on chapters 1 through 4 in The Way of Z.

Links to more Z lectures.

FORMAL METHODS

Apply logic and simple mathematics to computing.

Use formulas (symbols and rules).

Gain understanding through analysis rather than experiments (testing).

Can be applied to behavior (specification), structure (design, ``refinement''), implementation (verification).

Are most useful in projects that are novel, difficult, or critical.

GOALS OF FORMAL METHODS

Discover errors by analysis (earlier) instead of by testing or customer experiences (later).

Document development thoroughly to permit more objective technical evaluation and review (even automated analysis, machine checking).

FORMAL METHODS ARE *NOT* ...

Project management methods.

Useful for a nontechnical audience (customers, etc.)

Writing the program twice.

Replacements for all testing.

Replacements for creativity, judgment, experience.

Infallible (but some products can be *checked* more conclusively).

Automatic (but some products can be *checked* by machine).

Cost-effective for many routine projects.

WHAT IS A SPECIFICATION LANGUAGE

Formal syntax (like every programming language)

Formal semantics (unlike most programming languages):
you can *calculate* whether two formulas (specifications,
programs) mean the same thing by *formula manipulation*.

Describe states directly (not just state transitions).

Not necessarily executable.

Support automated analysis.

WHAT IS Z

Notational conventions for logic and simple mathematics.

Discrete mathematics with declarations and structure (``paragraphs'').

``Model-based'', with states and operations.

A notation, not a method.

Not specialized for any application.

Not a tool (but many tools available).

Not executable --- Z is not a programming language!

Z FEATURES

Non-ASCII (pictorial) symbols.

Relational calculus (data structures).

Schema calculus (large specifications).

Mathematical tool-kit (pre-defined objects and operators).

Literature, reference manual, draft ANSI/ISO standard.

Tools: typesetting, syntax and type checking, theorem proving, detetecting counterexamples.

Related notations (B, VDM, Object-oriented dialects).

APPLICATIONS OF FM

Some large projects have been fielded successfully:

IBM CICS transaction processing (Z)

Inmos Transputer FPU (Z, Occam)

Tektronix oscilloscopes (Z)

Paris Metro (B)

UK air traffic control (VDM)

DIFFICULTIES OF FM

Mathematical notation.

Abstraction (``story problems'').

Not executable (no trial-and-error).

More effort in early project stages.

Start from scratch.

Back to Z lectures.

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

E-mail: jon@u.washington.edu