Skip to navigation | Skip to main content | Skip to footer

COMP31111: Verified Development (2010-2011)

This is an archived syllabus from 2010-2011

Verified Development
Level: 3
Credit rating: 10
Pre-requisites: No Pre-requisites
Co-requisites: No Co-requisites
Lecturers: Richard Banach
Course lecturer: Richard Banach

Additional staff: view all staff
Sem 1 Lecture 1.4 Thu 15:00 - 17:00 -
Assessment Breakdown
Exam: 100%
Coursework: 0%
Lab: 0%

Themes to which this unit belongs
  • Rigorous Development


It has been known for a long time that, in theory, the whole activity of system specification, refinement and implementation, could be integrated into a comprehensive mathematical theory and could be supported by industrial strength system development tools. However an actual realisation of this supposition was slow to appear, and the idea was not really made practical until the mid 1980s. Nowadays though, there are a number of tools that embody this idea, and the integration of various reasoning technologies into the process (these days often behind the scenes) is a fertile area of research. This course is an introduction to this methodology.


This course is an introduction to verified development, using the Perfect Developer tool from Eschertech, which allows the development of abstract models, and their translation and refinement into running Java code.

Programme outcomeUnit learning outcomesAssessment
A1 A3 B1 D6Be familiar with informal and rigorous development.
  • Examination
A1 A3 B1 D6Be familiar with model based refinement.
  • Examination
A1 A3 B1 D6Have a knowledge of Perfect Developer.
  • Examination
A1 A3 B1 D6Be able to design and build simple applications using Perfect Developer.
  • Examination
A1 A3 B1 D6Have an appreciation of the significance of Perfect's verification conditions.
  • Examination


Overview of informal and rigorous development.
Overview of model based refinement.
Basics of the Perfect language.
Practical development and refinement in Perfect.
More refinement theory.
The role of automated reasoning.
Prospects for the future.

Reading List

There are no books specifically about Perfect Developer at present. Notes will be handed out in lectures, and are available on the course website, which also contains some suggestions for related reading.