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
Introduction
• 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 Examination | 70 |