% intro-slides.tex (root is intro.tex) \pagestyle{empty} \begin{slide}{} \begin{center} INTRODUCING Z Jonathan Jacky Radiation Oncology, Box 356043 \\ University of Washington \\ Seattle, Washington 98195-6043 \\ USA \vspace{1.0in} %http://www.radonc.washington.edu/prostaff/jon jon@radonc.washington.edu \end{center} \vspace{1.0in} \small{\copyright Jonathan Jacky 1997 \\ Do not copy without author's permission} \end{slide} \begin{slide}{} 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. \end{slide} \begin{slide}{} 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). \end{slide} \begin{slide}{} FORMAL METHODS ARE {\em NOT} \dots 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 {\em checked} more conclusively). Automatic (but some products can be {\em checked} by machine). Cost-effective for many routine projects. \end{slide} \begin{slide}{} WHAT IS A SPECIFICATION LANGUAGE Formal syntax (like every programming language) Formal semantics (unlike most programming languages): you can {\em calculate} whether two formulas (specifications, programs) mean the same thing by {\em formula manipulation}. Describe states directly (not just state transitions). Not necessarily executable. Support automated analysis. \end{slide} \begin{slide}{} 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! \end{slide} \begin{slide}{} 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). \end{slide} \begin{slide}{} 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) \end{slide} \begin{slide}{} DIFFICULTIES OF FM Mathematical notation. Abstraction (``story problems''). Not executable (no trial-and-error). More effort in early project stages. Start from scratch. \end{slide}