Module 08144 (2004)

Syllabus page 2004/2005

06-08144
Formal Methods
Level 3/H

Antoni Diller
10 credits in Semester 1

Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus

The Module Description is a strict subset of this Syllabus Page. (The University module description has not yet been checked against the School's.)

Relevant Links

Further information about this module, including any last-minute changes, corrections and alterations to the information contained above, can be found on my Formal Methods module web page .

Outline

The purpose of this module is to present a mathematically-based formal specification language and show how it is used to formally specify a software component. Methods of proving that the final program meets its specification will also be looked at.

Aims

The aims of this module are to:

  • present the basic ideas and some of the methods of mathematical modelling
  • show how a formal specification of a software component can be written
  • show how to refine a specification
  • show how to implement a specification in an imperative programming language
  • show how to animate a specification in a functional programming language
  • show how to reason about specifications

Learning Outcomes

On successful completion of this module, the student should be able to: Assessed by:
1 use the main operators of Z's mathematical toolkit (especially relational operators) Examination
2 write a formal specification of a software component in Z Examination
3 refine a high-level, abstract specification into a low-level, concrete one Examination
4 prove that a refinement is correct Examination
5 calculate the pre-condition schema of a schema Examination
6 work out what the composition of two schemas is Examination
7 translate a schema which is part of a low-level, concrete specification into a Hoare triple Examination
8 prove that a program fragment correctly implements a schema Examination
9 carry out simple proofs in a Hoare logic Examination
10 annotate a small imperative program Examination
11 calculate the verification conditions of a Hoare triple Examination
12 implement a formal specification Examination
13 prove that an implementation is correct Examination
14 animate a formal specification Examination
15 prove that a specification has various properties Examination
16 recognise deductivist style and be aware of its dangers Examination

Restrictions, Prerequisites and Corequisites

Restrictions:

None

Prerequisites:

None

Co-requisites:

None

Teaching

Teaching Methods:

Ten one-hour weekly lectures; revision lecture; lecturer access by appointment.

Contact Hours:

11+

Assessment

  • Supplementary (where allowed): As the sessional assessment
  • 2 hr examination (100%).

Recommended Books

TitleAuthor(s)Publisher, Date
Z: An Introduction to Formal Methods (second edition) Antoni Diller Wiley , 1994
Proofs and Refutations Imre Lakatos CUP , 1976
The Z Notation: A Reference Manual (second edition) J. M. Spivey Prentice Hall , 1992
Introduction to Functional Programming using Haskell (second edition) Richard Bird Prentice Hall , 1998
Haskell: The Craft of Functional Programming (second edition) Simon Thompson Addison Wesley Longman , 1999
Fatal Defect Ivars Peterson Vintage Books , 1996
Using Z: Specification, Refinement, and Proof Jim Woodcock and Jim Davies Prentice Hall , 1996
Introduction to Formal Methods A. Harry Wiley , 1996
An Introduction to Discrete Mathematics, Formal System Specification, and Z (second edition) D. C. Ince OUP , 1992

Detailed Syllabus

  1. Introduction: aims of the module; assessment; teaching methods; style of presentation; harmful effects of deductivist style and Euclidean methodology.
  2. Mathematical modelling: how mathematics is used to model software components and systems.
  3. Z's logical and mathematical toolkit: arithmetical relations and functions; propositional calculus, including useful laws; basic types (or given sets) and composite types, including set, Cartesian product and schema; typed predicate calculus; quantifiers, including restricted, unrestricted and unique; term-forming operators, including definite descriptions, conditional terms and local definitions; typed set theory; ways of making sets, including enumeration and comprehension; 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, including domain, range, inverse, image, domain restriction and anti-restriction, range restriction and anti-restriction, composition, powers, identity, closures (including transitive and reflexive-transitive) and overriding; simple proofs; functions (including partial, total, injective, surjective and bijective); sequences; and bags.
  4. 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; the Delta and Xi conventions; error schemas; partial and total specifications; several largish case-studies, including the internal telephone directory specification, a sales database, the bill of material problem, a route planner, Wing's library problem and a simple text-editor.
  5. Refinement: abstract and concrete specifications; bridging the gap between them; proof-obligations and how they are discharged, including correspondence of initial states, correctness and applicability of operations; reification; decomposition; the retrieve relation, function and schema.
  6. Verification: Hoare logic for a simple programming language including skip, assignment, sequencing, conditional, while-loop, repeat-loop, for-loop, procedures, functions, blocks and arrays; deriving a Hoare triple from a low-level Z specification; verification conditions; simple proofs; the philosophy of program verification; Fetzer and his critics; is certainty attainable?
  7. Animation: the ideas behind functional programming languages and their suitability for animation; animating a Z specification in Haskell; why Haskell is better for this than both Miranda (tm) and ML; representing the basic types, the state space and the initial state; translating operations into Haskell; the role of the state invariant.
  8. Other approaches: a look at the opposition, including Abrial's Abstract Machine Notation (AMN), B and VDM; why these are inferior to Z.

Last updated: 5 June 2003

Source file: /internal/modules/COMSCI/2004/xml/08144.xml

Links | Outline | Aims | Outcomes | Prerequisites | Teaching | Assessment | Books | Detailed Syllabus