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
• 8. cvičenie
• zobraz modul Ex08a - verifikácia programov: primitívna rekurzia
• zobraz modul Ex08b - verifikácia programov: 'course-of-values' rekurzia
• zobraz modul Ex08c - verifikácia programov: rekurzia s mierou
• zobraz modul Ex08d - verifikácia programov: iteratívna rekurzia
• 9. cvičenie
• zobraz modul Ex09a - verifikácia programov: zoznamy
• zobraz modul Ex09b - verifikácia programov: operácie na zoznamoch
• zobraz modul Ex09c - verifikácia programov: triedenie zoznamov
• 10. cvičenie
• zobraz modul Ex10 - verifikácia programov: binárne stromy
• 11. cvičenie*
• zobraz modul Ex11* - verifikácia programov: symbolické výrazy a numerické termy
• 12. cvičenie*
• zobraz modul Ex12 - aritmetizácia výpočtového modelu pre čiastočne rekurzívne funkcie

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