Department of Information Technology

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

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