Accessibility statement

Programming: Correctness by Construction - COM00012H

« Back to module search

  • Department: Computer Science
  • Module co-ordinator: Prof. Ana Cavalcanti
  • Credit value: 20 credits
  • Credit level: H
  • Academic year of delivery: 2021-22

Module will run

Occurrence Teaching period
A Autumn Term 2021-22 to Summer Term 2021-22

Module aims

Software should do what you expect as reliably as any other technology. Usually it does not, however. Software is often unreliable and fails to meet the requirements. Typical software defect rates are unacceptable for any other kind of product. This module covers the modelling, validation, design, and verification techniques that contemporary engineers can employ to save money and time, and reduce risks. Specific aims of this module are to:

  • Describe a coherent set of techniques and tools that support the practical development of programs correct by construction.
  • Cover sequential, concurrent, and reactive programs.
  • Discuss the principles that justify the main techniques.
  • Illustrate the techniques with realistic case studies.

Module learning outcomes

On completion of this module, students will:

  • Read and write descriptions of specifications and designs of sequential, concurrent and reactive systems;
  • Use animation to validate specifications and designs;
  • Understand the models that support program development;
  • Understand refinement as a relation that captures the concept of correctness in the various models;
  • Analyse specifications and verify designs using refinement and model checking;
  • Develop programs that are guaranteed to meet their contracts.

Assessment

Task Length % of module mark
Online Exam - 24 hrs (Centrally scheduled)
Programming: Correctness by Construction (PCOC1)		 8 hours 50
Online Exam - 24 hrs (Centrally scheduled)
Programming: Correctness by Construction (PCOC2)		 8 hours 50

Special assessment rules

None

Reassessment

Task Length % of module mark
Online Exam - 24 hrs (Centrally scheduled)
Programming: Correctness by Construction (PCOC1)		 8 hours 50
Online Exam - 24 hrs (Centrally scheduled)
Programming: Correctness by Construction (PCOC2)		 8 hours 50

Module feedback

Two formative assessments in the Autumn Term.
A number of formative assessments (typically four) in the Spring Term.

Indicative reading

*** Woodcock J.C.P. and Davies J., Using Z: specification, refinement and proof, Prentice-Hall International, 1996

*** A. W. Roscoe, Understanding Concurrent Systems, Springer, 2011


The information on this page is indicative of the module that is currently on offer. The University is constantly exploring ways to enhance and improve its degree programmes and therefore reserves the right to make variations to the content and method of delivery of modules, and to discontinue modules, if such action is reasonably considered to be necessary by the University. Where appropriate, the University will notify and consult with affected students in advance about any changes that are required in line with the University's policy on the Approval of Modifications to Existing Taught Programmes of Study.