Registry

Module Specifications

Current Academic Year 2012 - 2013
Please note that this information is subject to change.

Module Title	Formal Programming
Module Code	CA648
School	School of Computing
Online Module Resources
Module Co-ordinator	Semester 1: Geoffrey Hamilton Semester 2: Geoffrey Hamilton Autumn: Geoffrey Hamilton
Module Teacher	Geoffrey Hamilton
NFQ level	8	Credit Rating	7.5
Pre-requisite	None
Co-requisite	None
Compatibles	None
Incompatibles	None

Description

The module aims to enable students to use mathematical notations and techniques to enhance significantly the quality of the code they produce. They will acquire theoretical insight into the mathematics of specifying, verifying and constructing programs.

Learning Outcomes

1. Explain the roles of specification, verification and refinement in the process of developing correct software.
2. Specify programs in a precise formal notation.
3. Prove the correctness of programs with respect to their specifications.
4. Refine specifications in a precise mathematical framework.
5. Develop programs from their specifications which are correct by construction.

Workload	Full-time hours per semester
*Type*	*Hours*	*Description*
Lecture	36	No Description
Lecture	36	No Description
Independent learning	151	No Description
Independent learning	151	No Description
Total Workload: 374

All module information is indicative and subject to change. For further information,students are advised to refer to the University's Marks and Standards and Programme Specific Regulations at: http://www.dcu.ie/registry/examinations/index.shtml

Indicative Content and Learning Activities

The course will cover the following:.
- Formal logic- Sets, sequences, relations and functions- Floyd/Hoare Logic- Formal specification- Partial correctness- Total correctness- Program verification- Program refinement- Event-B.

Assessment Breakdown
Continuous Assessment	25%	Examination Weight	75%

Course Work Breakdown
Type	Description	% of total	Assessment Date
Assignment	Formal Specification of Programs	12%	Week 7
Assignment	Refinement of Specifications	13%	Week 11

Reassessment Requirement
Resit arrangements are explained by the following categories; 1 = A resit is available for all components of the module 2 = No resit is available for 100% continuous assessment module 3 = No resit is available for the continuous assessment component
This module is category 1

Indicative Reading List

Jean-Raymond Abrial: 2009, Modelling in Event-B: System and Software Engineering, 1, Cambridge University Press,
Roland Backhouse: 2003, Program Construction: Calculating Implementations from Specifications, 1, Wiley, 0-470-84882-0

Other Resources

None

Array

Programme or List of Programmes

BSSA

Study Abroad (DCU Business School)

CAPD

PhD

CAPM

MSc

CAPT

PhD-track