OHJ-2506 Program Verification, 2011 (P1, P2)

18.8.2011 page started.
23.8.2011 page published.
26.8.2011 lecture material added (in pdf form).
1.9.2011 fixed typo in calendar: exercise 8 is in Th 3.11.2011 (not 4.1.11)
1.9.2011 exercises 1 added
8.9.2011 the grading will be by exercises, no exam
9.9.2011 time for exercise session is decided: P1: on Thursdays at 16-18 (we start at 16.05), and P2: on Thursdays at 16-19 (we start at 16.05)
9.9.2011 exercises 2 added
16.9.2011 exercises 3 added
23.9.2011 exercises 4 added
30.9.2011 exercises 5 added
7.10.2011 exercises 6 added
20.10.2011 exercises 7 added
31.10.2011 exercises 8 added
7.11.2011 exercises 9 added
15.11.2011 exercises 10 added
21.11.2011 exercise 11 added
29.11.2011 exercises 12 added
5.12.2011 exercises 13 added

Description

The general goal of the course is to learn to use mathematically rigorous methods in software engineering, especially predicate logic and set theory. Learning outcomes are ability to verify parts of programs, algorithms and data structures using logic and set theory. We also study fundamental and practical limitations of the formal methods.

In the course we practise how to do logical calculations which can be little hard in the beginning if the student does not have any previous experience.

In the beginning of the course we repeat some things learned in the course OHJ-2100 Ohjelmistotieteen perustyökaluja (Basic Tools for Software Science) like predicate logic, set theory, and writing state predicates.

The course is valid for post-graduate studies.

Lectures

Lectures are given twice a week, on the 1. period two hours at a time, and on the 2. period the first lecture two hours and at the second lecture one hour.

lecturer: Antero Kangas, antero.kangas@tut.fi, TF 211
start: tuesday 30.8.2011
P1: Tuesday 12–14 (TC210) and Thursday 12–14 (TC103)
P2: Tuesday 12–14 (TC210) and Thursday 12–13 (TC103)

Exercises

Exercises are obligatory and probably the grades will be determined on the exercises (it depends on the number of participants). That will be decided during the first lectures.

Exercises are given on the 1. period two hours a week and on the 2. period three hours a week. There are no exercises on the first week.

Time for exercise sessions is decided.

the lecturer gives the exercises
starts: 8.9.2010
P1: on Thursday at 16–18 (TC103)
P2: on Thursday at 16–19 (TC103)

Please notive that the exercise sessions will start at 16.05!

The weekly exercises will be notified on this page:

Exercise #	Week	Date	Problems
1	36	8.9.2011	1-6
2	37	15.9.2011	7-12 (+6 as a personal task)
3	38	22.9.2011	9,10bc,11,12,13,14
4	39	29.9.2011	12,15,16-19
5	40	6.10.2011	18,19,20-23
6	41	13.10.2011	22,23,24-27
Exam week	42		No exercises
7	43	27.10.2011	26(defg),27,28-32
8	44	3.11.2011	32 (notice: it is slightly modified!), 33-37
9	45	10.11.2011	38-44
10	46	17.11.2011	43,44,45-48
11	47	24.11.2011	48,49-51
12	48	1.12.2011	52-55
13	49	8.12.2011	55,56-58. Notice that the program mentioned on problem 58 is in Section 5.1 Using an Abstract Data Structure, in the lecture material.

A link to the exercises in pdf form. Exercise groups in pdf:
(1-2) (1,2)
(1-3) (3)
(1-4) (4)
(1-5) (5)
(1-6) (6)
(1-7) (7)
(1-8) (8)
(1-9) (9)
(1-10) (10)
(1-11) (11)
(1-12) (12)
(1-13) (13)

The exercises will be given in the following way:

in the beginning of the exercise I call the names and ask which problems you have done, and pick the one who shall present her or his solution
the precedence is her or his who has least presented solutions (there may and will be exceptions)
if there reveals errors or weaknesses in the solution then
- the student may try to fix it himself,
- the problem can be given him as a personal task for the next time, or
- I shall pick someone else to present his solution

Be prepared to present your answers. It is better to do less carefully than much "poorly". The grade is not determined directly by the number of presented problems, but by solving only a few of the problems it is not possible to show what you have learned.

Timetable

The lectures begin on 30.8.2011 and the exercises on 8.9.2011

Timetable for period P1

	ti	to
8–9
9–10
10–11
11–12
12–13	Lecture TC210	Lecture TC103
13–14	Lecture TC210	Lecture TC103
14–15
15–16
16–17		Exercise TC103
17–18		Exercise TC103
18–19

Timetable for period P2

	ti	to
8–9
9–10
10–11
11–12
12–13	Lecture TC210	Lecture TC103
13–14	Lecture TC210
14–15
15–16
16–17		Exercise TC103
17–18
18–19

Calendar

Week 35: 29.8.–4.9.2011. Period P1 begins
Tu	30.8.2011	Lecture	12–14	TC210
Th	1.9.2011	Lecture	12–14	TC103
Week 36: 5.9.–11.9.2011
Tu	6.9.2011	Lecture	12–14	TC210
Th	8.9.2011	Lecture	12–14	TC103
Th	8.9.2011	Exercise 1	16–18	TC103
Week 37: 12.9.–18.9.2011
Tu	13.9.2011	Lecture	12–14	TC210
Th	15.9.2011	Lecture	12–14	TC103
Th	15.9.2011	Exercise 2	16–18	TC103
Week 38: 19.9.–25.9.2011
Tu	20.9.2011	Lecture	12–14	TC210
Th	22.9.2011	Lecture	12–14	TC103
Th	22.9.2011	Exercise 3	16–19	TC103
Week 39: 26.9.–2.10.2011
Tu	27.9.2011	Lecture	12–14	TC210
Th	29.9.2011	Lecture	12–14	TC103
Th	29.9.2011	Exercise 4	16–19	TC103
Week 40: 3.10.–9.10.2011
Tu	4.10.2011	Lecture	12–14	TC210
Th	6.10.2011	Lecture	12–14	TC103
Th	6.10.2011	Exercise 5	16–18	TC103
Week 41: 10.10.–16.10.2011
Tu	11.10.2011	Lecture	12–14	TC210
Th	13.10.2011	Lecture	12–14	TC103
Th	13.10.2011	Exercise 6	16–18	TC103
Week 42: 17.10.–23.10.2011
Exam week – no lectures, no exercises
Week 43: 24.10.–30.10.2011. Period P2 begins
Tu	25.10.2011	Lecture	12–14	TC210
Th	27.10.2011	Lecture	12–13	TC103
Th	27.10.2011	Exercise 7	16–19	TC103
Week 44: 31.10.–6.11.2011
Tu	2.11.2011	Lecture	12–14	TC210
Th	4.11.2011	Lecture	12–13	TC103
Th	4.11.2011	Exercise 8	16–19	TC103
Week 45: 7.11.–13.11.2011
Tu	8.11.2011	Lecture	12–14	TC210
Th	10.11.2011	Lecture	12–13	TC103
Th	10.11.2011	Exercise 9	16–19	TC103
Week 46: 14.11.–20.11.2011
Tu	15.11.2011	Lecture	12–14	TC210
Th	17.11.2011	Lecture	12–13	TC103
Th	17.11.2011	Exercise 10	16–19	TC103
Week 47: 21.11.–27.11.2011
Tu	22.11.2011	Lecture	12–14	TC210
Th	24.11.2011	Lecture	12–13	TC103
Th	24.11.2011	Exercise 11	16–19	TC103
Week 48: 28.11.–4.12.2011
Tu	29.11.2011	Lecture	12–14	TC210
Th	1.12.2011	Lecture	12–13	TC103
Th	1.12.2011	Exercise 12	16–19	TC103
Week 49: 5.12.–11.12.2011
Tu	6.12.2011	Independende Day, no lectures
Th	8.12.2011	Lecture	12–13	TC103
Th	8.12.2011	Exercise 13	16–19	TC103

The corresponding former courses

The course is exchangable in both directions with the older courses 8101160 Ohjelmien todistaminen and OHJ-2500 Ohjelmien todistaminen.

Grading

Evaluation criteria for the course are determined in the beginning of the course. The idea is that if there are not too many participants the grading can be determined by the exercises. Otherwise there will be an exam.

Grading will be determined by exercises and therefore there will be no exam.

Material

The English material can be found here

The former lecture material in Finnish is still valid and is sold in decreased form 4 --> 1 by TiTe.

The exercise problems will be delivered in this page, see Exercises.

Possible extra material will also be delivered in this page.

In the course we use the same notations as in course OHJ-2100 Ohjelmistotieteen perustyökaluja (Basic Tools for Software Science). Here are the descriptions of notations in English and in Finnish in PDF format.

Prerequisites

OHJ-2100 Ohjelmistotieteen perustyökaluja (Basic Tools for Software Science).