PSE214 FORMAL METHODS

Introduction: aims of the module; assessment;
teaching methods; style of presentation; harmful effects of deductivist style
and Euclidean methodology.

Mathematical Modeling: how mathematics is used to model software components and
systems.

Z's logical and mathematical toolkit: arithmetical relations and
functions; propositional calculus, relations between sets and their members;
operations on sets; some special sets; useful set-theoretic laws; relations,
including heterogeneous and homogeneous; the calculus of relations.

**Specification and the schema calculus**: state space; state schema; before
and after schemas; state invariant; operation schemas; schema operations,
including composition, piping, renaming, linking using propositional
connectives, inclusion, hiding, the theta-operator, and pre-condition
calculation.

**Refinement**: abstract and concrete specifications Verification: Hoare
logic for a simple programming language.

**Other approaches**: a look at the opposition, including Abrial's Abstract
Machine Notation (AMN), B and VDM Comparative analysis. Applications of Z.

*Recommended
Books*

*Antoni Diller; Z: An Introduction to Formal Methods (second edition), Wiley (1994).**J. M. Spivey, The Z Notation: A Reference Manual (second edition), Prentice Hall (1992).**Richard Bird; Introduction to Functional Programming using Haskell (second edition), Prentice Hall (1998) 2*^{nd}ed.*Simon Thompson, Haskell; The Craft of Functional Programming, Addison Wesley (1999) 2*^{nd}ed.*Jim Woodcock and Jim Davies; Using Z: Specification, Refinement, and Proof, Prentice Hall (1996) 2*^{nd}ed.*A. Harry; Introduction to Formal Methods, Wiley (2000).*