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

COMP31111 Verified Development syllabus 2017-2018

COMP31111 materials

COMP31111 Verified Development

Level 3
Credits: 10
Enrolled students: 2

Course leader: Richard Banach


Additional staff: view all staff

Additional requirements

  • Students who are not from the School of Computer Science must have permission from both Computer Science and their home School to enrol.

Assessment methods

  • 80% Written exam
  • 20% Coursework
Timetable
SemesterEventLocationDayTimeGroup
Sem 1 Lecture G36 Thu 15:00 - 17:00 -
Themes to which this unit belongs
  • Rigorous Development

Overview

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.

Aims

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.

Syllabus

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.

Teaching methods

Lectures

15

Laboratories

There are exercises associated with COMP31111. Some are to be submitted via Blackboard for assessment (counting 20% of the course).

Feedback methods

Feedback is provided face to face in the lab, and online for uploaded assessed materials.

Study hours

  • Assessment written exam (2 hours)
  • Lectures (22 hours)

Employability skills

  • Analytical skills
  • Innovation/creativity
  • Problem solving
  • Research

Learning outcomes

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
  • Lab assessment
A1 A3 B1 D6Be able to design and build simple applications using Perfect Developer.
  • Lab assessment
  • Examination
A1 A3 B1 D6Have an appreciation of the significance of Perfect's verification conditions.
  • Examination

Reading list

COMP31111 does not have a specified reading list.

Additional notes

Course unit materials

Links to course unit teaching materials can be found on the School of Computer Science website for current students.