FI:IV022 Design and Verification - Course Information

IV022 Design and verification of algorithms

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

prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.

Timetable

Thu 14:00–15:50 B011

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

• Applied Informatics (programme FI, B-AP)
• Applied Informatics (programme FI, N-AP)
• Information Technology Security (programme FI, N-IN)
• Bioinformatics (programme FI, B-AP)
• Bioinformatics (programme FI, N-AP)
• Information Systems (programme FI, N-IN)
• Informatics with another discipline (programme FI, B-BI)
• Informatics with another discipline (programme FI, B-FY)
• Informatics with another discipline (programme FI, B-GE)
• Informatics with another discipline (programme FI, B-GK)
• Informatics with another discipline (programme FI, B-CH)
• Informatics with another discipline (programme FI, B-IO)
• Informatics with another discipline (programme FI, B-MA)
• Informatics with another discipline (programme FI, B-SO)
• Informatics with another discipline (programme FI, B-TV)
• Informatics (programme FI, B-IN)
• Informatics (programme FI, M-IN)
• Informatics (programme FI, N-IN)
• Mathematical Informatics (programme FI, B-IN)
• Parallel and Distributed Systems (programme FI, B-IN)
• Parallel and Distributed Systems (programme FI, N-IN)
• Computer Graphics and Image Processing (programme FI, B-IN)
• Computer Graphics (programme FI, N-IN)
• Computer Networks and Communication (programme FI, B-IN)
• Computer Networks and Communication (programme FI, N-IN)
• Computer Systems and Data Processing (programme FI, B-IN)
• Computer Systems (programme FI, N-IN)
• Embedded Systems (eng.) (programme FI, N-IN)
• Programmable Technical Structures (programme FI, B-IN)
• Theoretical Informatics (programme FI, N-IN)
• Upper Secondary School Teacher Training in Informatics (programme FI, M-SS)
• Upper Secondary School Teacher Training in Informatics (programme FI, M-TV)
• Upper Secondary School Teacher Training in Informatics (programme FI, N-SS) (2)
• Artificial Intelligence and Natural Language Processing (programme FI, B-IN)
• Artificial Intelligence and Natural Language Processing (programme FI, N-IN)
• Image Processing (programme FI, N-AP)

Course objectives

The goal is to get acquaint with methods for design and verification of small sequential algorithms. The students acquire basic verification techniques.

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

Assessment methods (in Czech)

Zkouška je písemná a ústní. V případě zadání průběžných testů během semestru, mají tyto podíl nejvýše 30% na závěrečném hodnocení. Pomocné materiály nejsou povoleny.

Language of instruction

Czech

Further Comments

The course is taught annually.

Teacher's information

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

• Enrolment Statistics (Autumn 2007, recent)
  
• Permalink: https://is.muni.cz/course/fi/autumn2007/IV022