COMP3018J System Des & Verification

Academic Year 2024/2025

This module is intended to introduce students to the idea of the formal correctness of algorithms. It begins with a number of lectures and tutorials which show how to prove theorems in the predicate calculus. It next shows how to specify programs as Precondition/Postcondition pairs. We show how programs can be calculated from such specifications. We also show how we can generalise from these solutions to abstract problems and their solutions.

Show/hide contentOpenClose All

Curricular information is subject to change

Learning Outcomes:

Having attended this module, studied the material and done the exercises the student should....
Be able to construct proofs in predicate logic.
Be able to construct specifications for a range of problems.
Be able to calculate programs to meet these specifications.
Be able to apply generic solutions to specific instances of problems.

Student Effort Hours: 
Student Effort Type Hours
Autonomous Student Learning

80
Lectures

32
Tutorial

16
Total

128
Approaches to Teaching and Learning:
Lectures and Tutorials 
Requirements, Exclusions and Recommendations

Not applicable to this module.


Module Requisites and Incompatibles
Not applicable to this module.
 
Assessment Strategy  
Description Timing Component Scale Must Pass Component % of Final Grade In Module Component Repeat Offered

Not yet recorded.

Carry forward of passed components
No
 
Resit In Terminal Exam
Summer Yes - 2 Hour
Please see Student Jargon Buster for more information about remediation types and timing. 
Feedback Strategy/Strategies

• Group/class feedback, post-assessment

How will my Feedback be Delivered?

Not yet recorded.