Computer Science, Prifysgol Cymru Aberystwyth University of Wales
C333(h)* - Formal Methods in Software Engineering
Brief Description
The course develops more rigorously the
formal methods introduced in
C332(h)
.
As background to the formal methods in software engineering,
students are introduced to formal logic and some of its other
applications in Computer Science
Aims, Objectives, Syllabus, Booklist
Further Details
- Number of lectures
- 22
- Number of seminars/tutorials
- 4
- Number of practicals
- 0
- Coordinator
- Dr. Fred Long
- Other staff involved
- Not yet known
- Pre-requisites
-
C332(h)
- Co-requisites
- None
- Incompatibilities
- None
- Assessment
- Assessed coursework - 20%
Written exam - 80%
- Timing
- This half module is offered only in Term 2
Aims
This half unit aims to develop more rigorously the
formal methods introduced in
C332(h)
by
presenting mathematical logic in a more formal way,
illustrating a number of different logics, and by
showing some of the other applications of logic in
Computer Science.
Objectives
On successful completion of this course students should understand:
-
the nature of formal proof in the propositional
and predicate logics;
-
the need for the three valued logic of partial
functions and how to carry out formal proof in that logic;
-
the ideas behind correctness proofs of
computer code and how to carry out such proofs themselves;
-
how proof is applied to the data types of
VDM;
-
temporal logic and its application
to the specification of concurrent systems;
-
the applications of logic in resolution
theorem proving, logic programming, expert systems, and fuzzy
systems.
Syllabus
-
Propositional Calculus - 2 Lectures
-
Revision of formal logic. Truth tables. The logic of
propositions. Logical reasoning. Consistency, completeness, and
decidability.
-
Predicate Calculus - 4 Lectures
-
The language of predicates. The use of quantifiers.
Valuations and models. Deductions, axioms and proofs.
-
Correctness Proofs - 3 Lectures
-
Programming proof rules and their application in the
specification of computer systems.
-
The Logic of Partial
Functions - 2 Lectures
-
Proof in the three valued logic of partial functions.
Differences from the traditional two valued logic. Applications to
formal methods, in particular VDM.
-
Proof Involving VDM Data
Types - 5 Lectures
-
The VDM data types. Proof using the data types.
-
Temporal Logic - 2 Lectures
-
Specification of time dependent systems. The operators
always
,
sometimes
,
next
and
until
.
Extension of VDM to include temporal logic.
-
Logic
Applications in Computing - 4 Lectures
-
Resolution theorem proving. Logic programming and Prolog.
Multi-valued logics, Fuzzy logic, and reasoning with uncertainty.
Booklist
It is considered essential to purchase the following
-
R.D. Dowsing, V.J. Rayward-Smith, and C.D. Walter.
A First Course in Formal Logic and its Application in Computer
Science,.
Computer Science Texts. Blackwell Scientific Publications, 1986.
-
C.B. Jones.
Systematic Software Development Using VDM.
International Series in Computer Science. Prentice-Hall, 2nd.
edition, 1990.
The following should be consulted for different approaches or for further information
-
J. Woodcock and M. Loomes.
Software Engineering Mathematics.
Pitman, 1988.
J.M. Spivey.
The Z Notation: A Reference Manual.
International Series in Computer Science. Prentice-Hall, 2nd.
edition, 1992.
D. Bjø rner, C.A.R Hoare, and H. Langmaack, editors.
VDM '90: VDM and Z - Formal Methods in Software Development,
volume 428 of LNCS.
Springer-Verlag, 1990.
Version 2.1
Syllabus
Nigel Hardy Departmental Advisor
nwh@aber.ac.uk
Dept of Computer Science, UW Aberystwyth (disclaimer)