Department of Information Technology

# Programming Theory (1DT034 - 1DT007) 2011

## News

• You can find the re-exam date here. For now, it is planned for August 29th 2012 from 14 to 19 in Polacksbacken's skrivsal.

## Schedule

Date Time Room Type Content
31/08 15-17 1311 Lecture Introduction
02/09 13-15 1311 Lecture Proof Theory: Propositional Logic
06/09 13-15 6140 Lecture Proof Theory: Predicate Logic
08/09 13-15 1111 Lecture Arrays
14/09 15-17 1111 Tutorial Proof Theory
16/09 10-12 1111 Lecture Weakest Preconditions
20/09 13-15 1111 Lecture Programming Language
21/09 13-15 2247 Lecture The Assignment Command
27/09 08-10 1311 Lecture The Alternative Command
29/09 08-10 1311 Lecture The Iterative Command
07/10 13-15 1311 Tutorial Weakest Preconditions
11/10 13-15 1311 Lecture Total Correctness
27/10 13-15 1311 Tutorial Invariants - Total Correctness
02/11 13-15 1111 Tutorial Practice: Spec#
04/11 13-15 1311 Tutorial Practice: Spec# (Examples (1,2) and Q&A)
10/11 13-15 1313 Lab Session Lab: Spec#
23/11 10-12 1311 Tutorial previous final exams
05/12 13-15 1313 Lab Session Lab: Spec#
09/12 14-19 Polacksbacken, Skrivsal Exam
12/12 08-17 Oral exam Spec# lab 1
13/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. 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.