Programming Theory (1DT034) 2013

Schedule

Date	Time	Room	Type	Content
04/09	13-15	1145	Lecture	Introduction-Proof Theory
06/09	10-12	1145	Lecture	Proof Theory: Propositional Logic
09/09	13-15	1145	Lecture	Proof Theory: Predicate Logic
12/09	15-17	1145	Lecture	Arrays
16/09	15-17	1145	Tutorial	Proof Theory
17/09	10-12	1145	Lecture	Weakest Preconditions
24/09	08-10	1145	Lecture	Programming Language
25/09	15-17	1145	Lecture	The Assignment Command, The Alternative Command
02/10	10-12	1145	Tutorial	Weakest Preconditions
08/10	08-10	1145	Tutorial	Programming Language
11/10	10-12	1245	Lecture	The Iterative Command, Total Correctness
21/10	13-15	1145	Tutorial	Spec#
29/10	13-15	1145	Lecture	Synthesis
04/11	15-17	1312,1313	Lab Session	Lab: Spec#
11/11	13-15	1145	Tutorial	Invariants - Total Correctness
14/11	13-15	1312,1313	Lab Session	Lab: Spec#
28/11	13-15	1245	Tutorial	Handledning
11/12	08-17	Polacksbacken, Skrivsal	Exam

Description

Objective

In the study of algorithms and their realization in programs, there are certain fundamental concerns, including:

models of computations and semantics,
computational complexity,
specification methods,
design and synthesis,
testing, and
verification methods and tools.

In this course we study how to:

write rigorous descriptions of implementations and specifications of programs, and
verify programs, i.e. prove that the implementation of a program meets its specification

The approach we adopt is that of formal methods. Formal methods concern the use of mathematical techniques in the design and analysis of programs. We define a small imperative programming language and use the calculus of weakest preconditions (invented by E. W. Dijkstra) to explain the semantics of the language. We use predicate logic as our specification language. We introduce a proof style based on predicate logic, and employ it to carry out the verification of our programs.

Prerequisites

The student is assumed to have a background in programming and programming languages. A basic first year mathematical education including an introductory course in mathematical logic is required. The student should be familiar with first order predicate calculus including its semantics and proof theory. A course in program semantics is useful.

Teachers

Mohamed Faouzi Atig: Lecturer
Carl Leonardsson: teacher assistant
Othmane Rezine: Teacher assistant
Aleksandar Zeljic: Teacher assistant

Literature

D. Gries, The Science of Programming, Springer-Verlag.
Parosh A. A., Logic in Programming, compendium. Available from UTH-Gård, number 73 on this map.
How to write proofs

Past Exams

Past Exams, slightly different focus

Past exam (19951025)
Partial solutions to past exam (19951025)
Past exam (19960814)
Partial solutions to past exam (19960814) Observe that the use of the for all definition in the proof of lemma 1 for problem 1 is wrong. You would need to use conditional substitution together with the corresponding assumptions about m1,m2 and m3.

For the exam, you are not allowed to bring anything but writing material (pen, pencil, rubber). This sheet will be distributed at the exam, for your aid.

Bonus Assignments

You can earn up to 4 points (out of 100) in the final exam by answering correctly to the questions at the beginning of some of the lectures. You can also secure 12 points in the final exam by passing three home assignments.
You will probably find the guide on writing proofs to be of help for solving the problems. Hand in your assignments BEFORE the deadline, using Studentportalen. You should upload your assignment as a .pdf file, it is recommended that you use LaTeX. The deadlines are hard, no late submissions will be considered. The assignment is to be solved individually, meaning that you can discuss solutions with course mates, but not hand in identical solutions.

Labs

The labs will make use of the Spec# language from Microsoft Research. A number of exercises will have to be solved in order to pass the course. Exercises are to be handed in using studentportalen. The deadlines are strict and late submissions will be ignored.