Module: Formal Programming

Module Specifications..

Current Academic Year 2023 - 2024

Please note that this information is subject to change.

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

None
Array

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.

*Type*	*Hours*	*Description*
Workload	Full-time hours per semester
Lecture	36	No Description
Lecture	36	No Description
Independent Study	151	No Description
Independent Study	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%

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

Reassessment Requirement Type
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

Programme or List of Programmes

CAPD	PhD
CAPM	MSc
CAPT	PhD-track
ECSA	Study Abroad (Engineering & Computing)
ECSAO	Study Abroad (Engineering & Computing)
GTEC	Graduate Training Visitor Program (E&C)
MCM	M.Sc. in Computing

Date of Last Revision

16-SEP-08

Archives: