Department of Information Technology

# Programming Theory (1DT034) 2012

## News

• 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.

## Schedule

Date Time Room Type Content
03/09 15-17 1311 Lecture Introduction
07/09 10-12 2347 Lecture Proof Theory: Propositional Logic
12/09 08-10 1211 Lecture Proof Theory: Predicate Logic
14/09 10-12 2345 Lecture Arrays
18/09 08-10 1211 Tutorial Proof Theory
20/09 10-12 2347 Lecture Weakest Preconditions
24/09 08-10 1211 Lecture Programming Language
28/09 15-17 1211 Tutorial Weakest Preconditions
02/10 15-17 1111 Lecture The Assignment Command
03/10 08-10 1211 Lecture The Alternative Command
09/10 15-17 1311 Tutorial Programming Language
12/10 10-12 1211 Lecture Lecture9.pdf|The Iterative Command
15/10 08-10 1311 Lecture Total Correctness
22/10 10-12 1211 Tutorial Invariants - Total Correctness
31/10 13-15 1311 Lecture Synthesis
01/11 10-12 1311 Tutorial Practice: Spec Sharp
06/11 13-15 1311 Tutorial Practice: Spec#
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
04/12 08-17 Polacksbacken, Skrivsal Exam
17/12 08-17 Oral exam Spec# lab 1
18/12 08-17 Oral exam Spec# lab 2

## 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.

### Past Exams

#### Past Exams, slightly different focus

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 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.

### 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. The lab exercises, as well as some pointers to technical information about installation and use of Spec# are available here.