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.