GCO4013

Formal methods in software engineering

J Hurst

6 points
* 4 hours per week
* Second semester
* Gippsland and distance
* Prerequisites: GCO3811, MAT1077
* Prohibition: SFT3302

Objectives On completion of the subject students will understand the role and importance of formal specifications in software development; be familiar with an algebraic notation for specifying data types; be able to use the Z notation to specify a software system; be familiar with the process of refining a software specification into an algorithm; and be able to reason about the correctness of an algorithm with respect to a specification.

Synopsis Review of set theory, the predicate calculus, relations, relational algebra and formal specification concepts; algebraic and model based specifications. The Z notation, schemas, schema calculus, schema types and operations; data and algorithm design; data and operation refinement; proofs of correctness. The place of formal methods in software engineering practice.

Assessment Examination 40%
* Assignments 60%

Recommended texts

Dijkstra E W and Scholten C S Predicate calculus and program semantics Springer-Verlag, 1990
Diller A Z: An introduction to formal methods 2nd edn, Wiley, 1994
Horebeek I V and Lewi J Algebraic specifications in software engineering Springer-Verlag, 1998
Jones C B and Shaw R C Case studies in systematic software development Prentice-Hall, 1990
Potter B, Sinclair J and Till D An introduction to formal specifications and Z Prentice-Hall, 1991
Wordsworth J B Software development with Z Addison-Wesley, 1992