1-AIN-470 Špecifikácia a verifikácia programov LS 2024/25

Prednášky: štvrtok 13.10 2h, M-XI
Cvičenia: štvrtok 14.50 2h, M-XI
Konzultácie: pondelok 14.30 - 15.00 v m. I-16 alebo po dohode
Učiteľ: Ján Komara

Novinky

O kurze

Tu nájdete základné informácie: 1-AIN-470 Špecifikácia a verifikácia programov

Prednášky

Tu nájdete záznamy prednášok (slajdy). Sú priebežne dopĺňané.

Literatúra

• Ján Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
• Ján Kľuka. Prednášky z Úvodu do deklaratívneho programovania LS 2014/2015. (Adobe Acrobat Document)
• Ján Komara. Recursive Functions. Lecture notes for the course 2-INF-264 Theory of Declarative Programming Winter 2015/16.

Cvičenia

• 1. cvičenie
• zobraz modul Ex01a - začíname s CL
• zobraz modul Ex01b - explicitné definície
• zobraz modul Ex01c - rekurzívne definície
• 2. cvičenie
• zobraz modul Ex02a - celočíselná odmocnina (názorný príklad)
• zobraz modul Ex02b - Cantorova párovacia funkcia a aritmetizácia karteziánskeho súčinu
• zobraz modul Ex02c - Catalanova párovacia funkcia
• 3. cvičenie
• zobraz modul Ex03a - zoznamy
• zobraz modul Ex03b - triedenie zoznamov
• zobraz modul Ex03c - kombinatorické funkcie na zoznamoch
• 4. cvičenie
• zobraz modul Ex04a - binárne stromy
• zobraz modul Ex04b - binárne vyhľadávacie stromy
• 5. cvičenie
• zobraz modul Ex05 - symbolické výrazy a numerické termy
• 6. cvičenie
• zobraz modul Ex06a - výroková logika
• zobraz modul Ex06b - výrokovo-logické vyplývanie
• 7. cvičenie*
• zobraz modul Ex07a* - logická platnosť a logické vyplývanie
• zobraz modul Ex07b* - verifikácia programov: explicitné definície

Hodnotenie

Spôsob hodnotenia:

• A = aspoň 90 bodov

• B = aspoň 80 bodov

• C = aspoň 70 bodov

• D = aspoň 60 bodov

• E = aspoň 50 bodov

Toto je len základný rámec, spresnenie na 1. prednáške.

Softvér

Tu nájdete pokyny ako si nainštalovať softvér, ktorý budeme používať pri výučbe.

Staršie správy