| Module Title |
Formal Programming |
| Module Code |
CSC1136 (ITS: CA648) |
|
Faculty |
Engineering & Computing |
School |
Computing |
|
NFQ level |
9 |
Credit Rating |
7.5 |
|
|
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 | | Independent Study | 151 | No Description | | Lecture | 36 | No Description | | Independent Study | 151 | No Description |
| Total Workload: 374 |
|
|
| Section Breakdown | | CRN | 20410 | Part of Term | Semester 2 | | Coursework | 25% | Examination Weight | 75% | | Grade Scale | 40PASS | Pass Both Elements | N | | Resit Category | RC1 | Best Mark | N | | Module Co-ordinator | Geoffrey Hamilton | Module Teacher | |
|
| Assessment Breakdown |
| Type | Description | % of total | Assessment Date |
|---|
| Assignment | Formal Specification of Programs | 12% | Week 7 | | Assignment | Refinement of Specifications | 13% | Week 11 | | Formal Examination | End-of-Semester Final Examination | 75% | End-of-Semester |
| Reassessment Requirement Type |
Resit arrangements are explained by the following categories;
RC1: A resit is available for both* components of the module.
RC2: No resit is available for a 100% coursework module.
RC3: No resit is available for the coursework component where there is a coursework and summative examination element.
* ‘Both’ is used in the context of the module having a coursework/summative examination split; where the module is 100% coursework, there will also be a resit of the assessment
|
|
Pre-requisite |
None
|
|
Co-requisite |
None |
| Compatibles |
None |
| Incompatibles |
None |
|
|
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
Error parsing Indicative Content: Syntax error - 4 |
Indicative Reading List
Books:
- 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
Articles:
None |
Other Resources
None |
|
|
|
|
