Module: Formal Programming

Module Specifications.

Current Academic Year 2024 - 2025

All Module information is indicative, and this portal is an interim interface pending the full upgrade of Coursebuilder and subsequent integration to the new DCU Student Information System (DCU Key).

As such, this is a point in time view of data which will be refreshed periodically. Some fields/data may not yet be available pending the completion of the full Coursebuilder upgrade and integration project. We will post status updates as they become available. Thank you for your patience and understanding.

Date posted: September 2024

Module Title	Formal Programming
Module Code	CA648 (ITS) / CSC1136 (Banner)
Faculty	Engineering & Computing	School	Computing
Module Co-ordinator	Geoffrey Hamilton
Module Teachers	-
NFQ level	9	Credit Rating	7.5
Pre-requisite	Not Available
Co-requisite	Not Available
Compatibles	Not Available
Incompatibles	Not Available

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: Resit category 1: A resit is available for both* components of the module. Resit category 2: No resit is available for a 100% continuous assessment module. Resit category 3: No resit is available for the continuous assessment component where there is a continuous assessment and examination element.
* ‘Both’ is used in the context of the module having a Continuous Assessment/Examination split; where the module is 100% continuous assessment, there will also be a resit of the assessment
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