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.