Object-oriented software development to an equivalent of SCQF Level 8

This module aims to provide you with a strong formal methods underpinning for usage in
real world software development problems. By integrating an industrial tool and
technique into your existing software development skills, you will learn to reason about
and develop your software in a more correct and reliable manner. The module itself
forms around a technology which can be integrated into a software development
process. Ada-SPARK is a formal language of component / object based systems, with
an underpinning in formal mathematical models. Various levels of formality are provided
within Ada-SPARK, from absence of runtime errors (AoRTE), through to full proof of
functional specifications. You will experience the differing amount of effort to
achieve each level. The module covers two main streams. A mathematical underpinning
for software development is provided via material presented on logic, set theory, and
proof. Ada-SPARK, used in safety-critical industrial applications, is introduced, and
forms the basis of the coding instruction. The module covers the following topics:

• Formal methods and their usage in industry and software development in general
• Ada as a programming language
• Ada-SPARK to support reliable and correct software development
• Logic, set theory, and proof theory
• Structuring complex software
• Proving program correctness via preconditions and proof obligations

Upon completion of this module you will be able to
LO1: Produce a design and specification for an application using a formal approach
LO2: Plan and develop an application which conforms to the obligations defined in a
formal design and specification
LO3: Critically assess the advantages and disadvantages that formal methods bring to
the software development process
LO4: Evaluate formal methods in comparison with other software development
processes and development methodologies
LO5: Integrate a formal approach into an existing software development process