Level B

(taught in English)

5 points, period 2, spring 2000


Pierre Flener, PhD, Docent
Pierre.Flener at it.uu.se

Goals & Approach

The first goal is to understand the need for correct programming without testing, the need for precise specifications, as well as the inherent difficulties of correct programming. The second goal is to study two techniques of explicitly and rigorously constructing programs that correctly meet their specifications.

Special care is taken not to introduce any formal notations, as we are not interested here in computer-aided verification, nor in automated programming. All specifications are thus written in English, and all reasoning is conducted in English, relying on common sense. (Only knowledge of basic arithmetic is assumed here, considering the chosen examples.) This approach naturally scales up to programming-in-the-large.


There currently is no textbook teaching this material in the non-formal approach taken here. To avoid confusion, it is recommended not to read any of the existing textbooks until the course is over and its main message understood.

Some slides (but not all the material) for the lectures are available online.

Lessons & Labs & Project

In the lessons, either the instructor solves exercises in front of the whole class, or a designated student team shows its prepared solution to an exercise in front of the rest of the class, guided by the instructor (if need be). Exercises are assigned at least one week in advance. Since it is nearly impossible to understand the course material without personally trying the exercises, it is highly recommended to come prepared to the lessons, and to attend them all.

There are no labs with experiments on computers, because of the paper-and-pencil approach taken here.

There is no project, because the nature and novelty (to most students) of the course material make it impossible to solve a major problem in only 5 weeks.


Day Hours Location Type Content
Tue 22 Feb 8:15-10am A122 lecture 1 Introduction-1
Wed 23 Feb 8:15-10am B119 lecture 2 Introduction-2
Fri 25 Feb 8:15-10am B119 lecture 3 Proving Programs by Computational Induction
Mon 28 Feb 8:15-10am B119 lecture 4 Constructing Programs by Comp'l Induction
Wed 1 March 8:15-10am B119 lesson 1 Exercise 1 and Exercise 2 (by the instructor)
Fri 3 March 8:15-10am B125 lesson 2 Exercise 3 and Exercise 4 (by students)
Mon 6 March 8:15-10am B119 lesson 3 Exercise 5 and Exercise 6 (by students)
Wed 8 March 8:15-10am B125 lecture 5 Proving Programs by Structural Induction
Fri 10 March 8:15-10am A122 lecture 6 Constructing Programs by Struct'l Induction
Mon 13 March 8:15-10am A122 lesson 4 Exercise 7 and Exercise 8 (by the instructor)
Wed 15 March 8:15-10am A122 lesson 5 Exercise 9 and Exercise 10 (by students)
Fri 17 March 8:15-10am A122 lesson 6 Exercise 11 and Exercise 12 (by students)
Mon 20 March 8:15-10am A122 lecture 7 Conclusion and Questions & Answers

Office Hours

The instructor holds an office hour immediately after the last lecture of each week, in his office (A321).

Teaching Assistant

There is no teaching assistant. See the instructor during his office hours (see above) with your questions.


The first exam will be on Thu 23 March, from 9am to 1pm, in Postscriptum Room 2, over the entire course material.

The second exam will be on Sat 15 April, from 9am to 1pm, in Postscriptum Room 1, over the entire course material.

Last updated 3 March 2000.