Program Reasoning

Module aims

In this module you will have the opportunity to:

  • use the principle of induction to reason about the correctness of functional programs
  • use pre, post and mid conditions and loop variants and invariants to reason about the correctness of object-oriented Programs
  • use the reasoning methods you have learned to establish the correctness of some fundamental algorithms in Computing

Learning outcomes

Upon successful completion of this module you will be able to:

  • identify and apply the correct form of induction to prove a mathematical property
  • apply structural induction to reasoning about the correctness of functional functions
  • construct an induction principle to reason about any data-type or relation
  • provide suitable pre-, post- and mid-conditions and loop variants and invariants to program fragments
  • prove the correctness of an object-oriented program following the Hoare Logic style
  • prove the correcntess of fundamental algorithms, e.g. for searching and sorting

Module syllabus

  • Mathematical induction, structural induction and induction over relations
  • Derivation of induction principles for arbitrary data-types and relations
  • Inductive reasoning applied to functional programs
  • Hoare Logic  for specifying pre-, post- and mid-conditions
  • Loop invariants and variants
  • Logical reasoning applied to object-oriented program 
  • Application of program reasoning to classical algorithms in Computing           

Teaching methods

The content of this module will be covered through a series of classroom sessions that combine traditional lectures and problem solving applied to formative, unassessed exercises. The lectures will make frequent use of Mentimeter to support in-class Q&A and Piazza will be used to support out-of hours discussion. Approximately half of the formative exercises will be covered in small-group tutorials, Personal Maths Tutorials (PMTs), which are weekly one-hour tutorials run by academic tutors and Undergraduate Teaching Assistants (UTAs). These tutorials encourage group discussions and group problem solving designed to reinforce your understanding of key topics in logic, discrete mathematics, algorithm design and program reasoning.                     


Coursework exercises will be written assignments that are based on elements of the programming exercise you will be working on as part of your laboratory work. This work will be assessed off-line by Graduate Teaching Assistants (GTAs).  All GTAs received extensive guidance on the marking criteria and a selection of all work is moderated by the course leads for consistency. The formative exercises selected for the PMT tutorials will be assessed by your academic tutor and UTA. This assessment does not count to your final degree mark, but is intended to give you an indication of how well you are assimilating the material taught and how effectively you are applying that material to solving previously unseen problems.              

Detailed feedback, both written and verbal, will be given on the  exercises covered in the PMT tutorials. These exercises will be issued approximately every two weeks and written feedback will be returned the week after submission. You will receive written feedback on the assessed coursework exercises.                   

Module leaders

Dr Mark Wheelhouse
Professor Sophia Drossopoulou