Sémantika programů - NSWI162

• Anglický název: Program Semantics
• Zajišťuje: Katedra distribuovaných a spolehlivých systémů (32-KDSS)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2020
• Semestr: zimní
• E-Kredity: 1
• Rozsah, examinace: zimní s.:0/1, Z [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština
• Způsob výuky: prezenční
• Způsob výuky: prezenční
• Další informace: http://d3s.mff.cuni.cz/teaching/program_semantics/
• Garant: doc. RNDr. Jan Kofroň, Ph.D.
• Třída: Informatika Bc.
• Kategorizace předmětu: Informatika > Softwarové inženýrství
• Neslučitelnost : NSWE002
• Záměnnost : NSWE002

Anotace

čeština

Poslední úprava: Tajemník Katedry (03.05.2017)

Cílem kurzu je seznámit studenty se základy sémantiky imperativních programovacích jazyků. Studenti budou seznámeni s nástrojem pro verifikaci vlastností programů. Zápočet bude udělen za vypracování dvou domácích úloh malého rozsahu.

angličtina

Poslední úprava: Tajemník Katedry (03.05.2017)

The goal of the course is to introduce the foundation of program semantics, especially those of imperative programmning languages. A tool for verification of program properties will be introduced. The credits will be given for making two small homeworks.

Podmínky zakončení předmětu

Poslední úprava: doc. RNDr. Jan Kofroň, Ph.D. (06.10.2017)

Pro získání zápočtu je nutné vypracovat zadané domácí úlohy v termínu. Z povahy věci tedy není možné zápočet opakovat.

Literatura

čeština

Poslední úprava: Tajemník Katedry (03.05.2017)

A. R. Bradley, Z. Manna: The Calculus of Computation, Springer-Verlag, 2007

E. M. Clarke, O. Grumberg, D. A. Peled: Model Checking, MIT Press, 1999

Požadavky ke zkoušce

Poslední úprava: doc. RNDr. Jan Kofroň, Ph.D. (03.10.2017)

Pro získání zápočtu je nutné vypracovat zadané domácí úlohy v termínu.

Sylabus

čeština

Poslední úprava: Tajemník Katedry (03.05.2017)

1) Představení pojmu sémantiky programů

2) Metody specifikace vlastností imperativních programů

3) Matematické základy specifikace

4) Dokazování vlastností programů

angličtina

Poslední úprava: Tajemník Katedry (03.05.2017)

1) Introduction to program semantics

2) Methods for property specification

3) Mathematical means for specification

4) Proving of program properties