Computer Science, Prifysgol Cymru Aberystwyth University of Wales
CS33310 (1995-96 session)
Formal Methods in Software Engineering
Brief Description
The course develops more rigorously the formal methods
introduced in
CS33210
. 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
- 24
- Number of seminars/tutorials
- 4
- Number of practicals
- 0
- Coordinator
- Dr. Fred Long
- Other staff involved
- Not yet known
- Pre-requisites
-
CS33210
- Co-requisites
- None
- Incompatibilities
- None
- Assessment
- Assessed coursework - 20%
Written exam -
80%
- Timing
- This module is offered only in Semester 2
Aims
This module aims to develop more rigorously the formal methods
introduced in
CS33210
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 4.2
Syllabus
John Hunt Departmental Advisor
jjh@aber.ac.uk
Dept of Computer Science, UW Aberystwyth (disclaimer)