Provably correct software
How do you write software that absolutely must be correct?
Computer software is increasingly being used in applications where failure can cause loss of life or major economic damage. We know that a major source of software problems are caused by poor requirements specifications. We also know that testing can never be exhaustive. A way around these difficulties is to write requirements specifications in mathematical notation rather than natural language and to use mathematical techniques to prove that a program functions in accordance with its specification. Such formal methods are increasingly being used in industry for the development of safety-critical applications such as aircraft control systems and railway signalling systems, but also for the development of complex microelectronic circuits such as microprocessors. This course will focus on how to construct requirements specifications in mathematical notation and how to use them to prove programs correct. We will study a particular notation and method (e.g. the "B" method and notation) and how it is used.
We will also use formal methods development tools to keep track of the work and assist in carrying out the proofs. By the end of the course, you will have written a formal specification for a simple application and developed a program which provably works in accordance with that specification. You will also have learned the basic theory and principles behind formal methods. Prerequisites: Methods of programming DV1, Algebra DV1, Logic och proof techniques DV1, Algorithms and data structures DV1 (or equivalent courses). Semantics and principles of programming languages DV1 is recommended.
Goal: Learn how to write programs which run correctly the first time without testing or debugging!