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 2024
• Semestr: zimní
• E-Kredity: 1
• Rozsah, examinace: zimní s.:0/1, Z [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: nevyuč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
• Je záměnnost pro: NSWI183

Anotace

čeština

Kurz nahrazen kurzem NSWI183. 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.

Poslední úprava: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

angličtina

The course replaced by NSWI183. 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.

Poslední úprava: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

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

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.

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

Literatura

čeština

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

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

Požadavky ke zkoušce

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

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

Sylabus

čeština

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

2) Metody specifikace vlastností imperativních programů

3) Matematické základy specifikace

4) Dokazování vlastností programů

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

angličtina

1) Introduction to program semantics

2) Methods for property specification

3) Mathematical means for specification

4) Proving of program properties

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