SUBJECT

Title

Theory of programming

Type of instruction

lecture + practical

Level

master

Faculty

Faculty of Informatics

Part of degree program

Credits

Recommended in

Semester 1

Typically offered in

Autumn semester

Course description

Basic notions of programming. The syntax and semantics of nondeterministic programs. Partial and total correctness. Weakest precondition. The notion of loop invariant. Derivation rules of program constructs. Verification: a method for proving total correctness of deterministic and nondeterministic programs. Synthesizing correct sequential programs by using the derivation rules. The correctness of concurrent programs, verification rules of the new statements (parbegin/parend, await). Owicki-Gries method for proving the total correctness of parallel programs, deadlock freedom and interference freedom.

Readings

K. R. Apt, E.-R. Olderog. Verication of Sequential and Concurrent Program. Springer-Verlag, 1997.
S. Owicki, D. Gries. An axiomatic proof technique for parallel programs. Acta Inf., 6, pp. 319-340, 1976
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, New York, 1976.