IV022 Návrh a verifikace algoritmů

Fakulta informatiky
jaro 2019
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
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Út 19. 2. až Út 14. 5. Út 12:00–13:50 B411
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
předmět má 40 mateřských oborů, zobrazit
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.
Výstupy z učení
Na konci tohoto kurzu bude student schopen navrhovat malé sekvenční algoritmy a dokazovat jejich správnost.
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
Výukové metody
přednáška, domácí cvičení, samostatné studium
Metody hodnocení
Zkouška je písemná. 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.
Informace učitele
http://www.fi.muni.cz/usr/brim/iv022.html
Další komentáře
Studijní materiály
Předmět je vyučován jednou za dva roky.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2007, jaro 2013, jaro 2015, jaro 2017, jaro 2018, jaro 2020, jaro 2021, podzim 2022, podzim 2023.