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

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