FI:IV022 Verification - Course Information

IV022 Design and verification of algorithms

Faculty of Informatics
Autumn 2002

Extent and Intensity

2/0. 2 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: z (credit).

Teacher(s)

prof. RNDr. Luboš Brim, CSc. (lecturer)

Guaranteed by

Timetable

Thu 10:00–11:50 B204

Prerequisites (in Czech)

Course Enrolment Limitations

The course is also offered to the students of the fields other than those the course is directly associated with.

fields of study / plans the course is directly associated with

Course objectives (in Czech)

Cílem předmětu je seznámit se s metodami návrhu a verifikace malých sekvenčních algoritmů. Studenti si osvojí základní verifikační techniky.

Syllabus

Programs as predicate transformers, weakest precondition, properties of predicate transformers, program correctness.
Garded command language. Skip and abort commands, composition, alternative command, iterative command.
Verification of programs, proof outlines, verification rules for sequential composition, alternative, and loop commands. Array manipulation.
Constructive verification of programs, basic principles and strategies, developing loops from invariants and bounds, developing invarinats.
Examples of program development. Deriving of efficient algorithms, Searching and sorting.

Literature

DIJKSTRA, Edsger W. and W. H. J. FEIJEN. A method of programming. Wokingham: Addison-Wesley Publishing Company, 1998, vii, 188 s. ISBN 0-201-17536-3. info
KALDEWAIJ, A. Programming :the derivation of algorithms. New York: Prentice Hall, 1990, xii, 216 s. ISBN 0-13-204108-1. info
GRIES, David. The Science of Programming. New York: Springer-Verlag, 1981, 366 s., ob. ISBN 0-387-90641-X. info

Language of instruction

Czech

Further Comments

The course is taught annually.

Teacher's information

http://www.fi.muni.cz/usr/brim/I022/