Derivation of Algorithms (G52DOA)

In Derivation of Algorithms you will learn how to use mathematics and formal logic to construct algorithms and to prove that they are correct. The starting point in the design of a program is a precise description of what it is supposed to do, formulated in a rigorous language. This description is called the specification of the program. We use precise methods to derive or calculate a realization of the specification. The final product is an algorithm that implements the requirements expressed by the specification. It is automatically correct, because we obtained it by accurate mathematical reasoning.

Outline of lectures

In this section you will find, after each lecture, a list of topics that were taught and links to additional material and lecture notes.

Date	Topics	Lecture Notes
1. 4 Feb 2010	Correctness of programs Testing vs. Formal Verification Informal example: Dictionary search	Lecture 1
2. 5 Feb 2010	Example of formal verification Dutch Flag Algorithm	Lecture 2
3. 11 Feb 2010	Review of Propositional Logic Natural Deduction: Conjunction and Implication	Lecture 3
4. 12 Feb 2010	Natural Deduction: Negation and Disjunction
5. 18 Feb 2010	Natural Deduction: Quantifiers	Lecture 5
6. 19 Feb 2010	Introduction to ProofWeb
7. 25 Feb 2010	Graph Models Completeness Theorems
8. 26 Feb 2010	Substitution Equality rules	Truth tables for predicate logic
9. 4 Mar 2010	Hoare Logic	Hoare Logic and Proof Tableax
10. 5 Mar 2010	Proof Tableaux
11. 11 Mar 2010	Weakest Preconditions Loop Invariants	Proof Tableax for While Loops
12. 12 Mar 2010	Examples of correctness proof for WHILE programs
13. 18 Mar 2010	Total Correctness of While Loops	Total Correctness
14. 19 Mar 2010	Example: Minimal Section Algorithm	Sections

Coursework and Tutorials

In this section you fill find the coursework that you have to complete as part of the requirement for this module. Your result in the coursework will contribute 25% of your final mark.

Coursework (deadline: 12 March)

The coursework consists in proving some propositions in natural deduction. You do this online using ProofWeb: after logging in, you will presented with a list of exercises to solve. Consult the manual to learn how to use ProofWeb.
Tutorials on Monday 22 February, 1, 8, 15, 22 and 29 March.

Examination

Here are some exercises, a model exam and both the exams from last year:

Contacting the teacher

Please don't hesitate to ask me any question you may have about the module. You can contact me during or just after lectures, by e-mail, or by coming to my office (A07 in the Computer Science building). If you send me an email, please put G52DOA in the subject line, so I know immediately that it is about this module.