FI:IV022 Návrh a verifikace algoritmů

IV022 Návrh a verifikace algoritmů

Fakulta informatiky
podzim 2002

Rozsah

2/0. 2 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

Rozvrh

Čt 10:00–11:50 B204

Předpoklady

! I022 Návrh a verifikace algoritmů

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.

Mateřské obory/plány

Cíle předmětu

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.

Osnova

Programy jako transformátory predikátů. Nejslabší vstupní podmínka (wp), vlastnosti transformátorů, správnost algoritmu.
Programovací jazyk GCL. Syntaxe, definice sémantiky pomocí transformátorů predikátů, SKIP, ABORT, vícenásobné přiřazení, sekvence, alternativa, cyklus.
Programátorská logika. Zákon sekvence, zákon alternativy, zákon cyklu, vektorové proměnné.
Návrh algoritmů. Principy a strategie pro návrh založené na programátorské logice, zákon současného návrhu a verifikace.
Příklady aplikace metodologie na návrh konkrétních algoritmů. Návrh efektivních algoritmů, vyhledávání a třídění.

Literatura

DIJKSTRA, Edsger W. a 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

Informace učitele

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

Další komentáře

Předmět je vyučován každoročně.