Module Overview

Derivation of Algorithms

The purpose of this module in formal design is to show how formal methods can be used to develop programs from specification and how to integrate the task of providing program correctness with that of program development.By applying the given methodologies to a number of different problem domains students will appreciate the value of applying academically rigorous techniques on real software development applications.The aims therefore are:- To provide learners with an understanding of art and science of deriving efficient algorithms that meet their specification- To show how algorithms can be proven to be correct by mathematical methods- Deepen learners understanding of programming techniques

Module Code

COMP H4018

ECTS Credits


*Curricular information is subject to change


• Motivation for formal approach to program development • Review of Predicate Calculus

Guarded Commands

• Pre.Post condition semantics of programs • Syntax and Axiomatic semantics of guarded command language • Concept of constructing program and proof obligations concurrently

Derivation Techniques

Construct programs formally using the following strategies: • Taking a conjunct as an invariant • Replacing constants with variables • Strengthening invariants • Tail invariants

Problem Domains

Formaly derive solutions to the following classes of problems: • Searching • Segmentation problems • Sequences and sorting

Deriving Efficient Programs

• Using the methodologies to derive O (log N) solutions

Module Content & Assessment
Assessment Breakdown %
Other Assessment(s)30
Formal Examination70