This is an advanced course teaching how to design algorithms and programs that are guaranteed to meet their specification. Starting with a mathematical description of the program's requirements, the course presents a formal method for turning such specifications into actual code, in a stepwise approach known as refinement. Techniques of algorithm refinement are presented, for the derivation of loops and recursive procedures from invariants. The developed algorithms are typically very short, but challenging, as we aim to construct correct and efficient code. The taught material is mainly based on the textbook "Programming from Specifications" by Carroll Morgan.
The following topics will be covered, along with a range of examples and case studies:
- Program specification using predicates and assertions: predicate notation, preconditions and postconditions, specification statements.
- A language based on guarded commands (featuring an assignment statement, sequential composition and conditional statements, blocks, local variables, and arrays) with proof rules for each program construct.
- Basic techniques for finding invariants.
- Constructed types: from sets, bags, and lists to functions and relations.
- Procedures, parameter passing, and reuse.
- Recursive procedures: rigorous derivation of sorting and search algorithms.
- Recursive types: linked lists and binary trees.
This repository includes the assignment of the course written in Dafny or SPARK.
Assignment 1:
Assignment 2 (Final Assignment):