Programming Theory (1DT034) 2012
- Very important: fill in the ANONYMOUS evaluation form here
- Results of the second bonus assignment can be found on the Student portal. Comments regarding the second bonus assignment can be found here
- All quizzes are now corrected and can be picked up from the binder marked "PT2012" located in the window in the northern end on the corridor on the fourth floor of house 1. You can also find your final grades for the quizzes using Studentportalen.
- A list of Axioms and Inference Rules is available here. Only this list will be distributed at the exam, for your aid.
|07/09||10-12||2347||Lecture||Proof Theory: Propositional Logic|
|12/09||08-10||1211||Lecture||Proof Theory: Predicate Logic|
|02/10||15-17||1111||Lecture||The Assignment Command|
|03/10||08-10||1211||Lecture||The Alternative Command|
|12/10||10-12||1211||Lecture||Lecture9.pdf|The Iterative Command|
|22/10||10-12||1211||Tutorial||Invariants - Total Correctness|
|01/11||10-12||1311||Tutorial||Practice: Spec Sharp|
|08/11||13-15||1312D, 1313D||Lab Session||Lab: Spec#|
|15/11||13-15||1312D, 1313D||Lab Session||Lab: Spec#|
|22/11||13-15||1312D, 1313D||Lab Session||Lab: Spec#|
|27/11||10-12||1311||Tutorial||previous final exams|
|17/12||08-17||Oral exam||Spec# lab 1|
|18/12||08-17||Oral exam||Spec# lab 2|
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.
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.
- Mohamed Faouzi Atig: Lecturer
- Othmane Rezine: Teacher assistant
- Aleksandar Zeljic: Teacher assistant
- 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 exam (20111209)
- Past exam (20081216)
- Partial solutions to past exam (20081216)
- Past exam (042010)
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.
You can earn 1 point (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.
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. The lab exercises, as well as some pointers to technical information about installation and use of Spec# are available here.