1-AIN-470 Špecifikácia a verifikácia programov LS 2022/23

Prednášky: pondelok 9.50 2h, M-XI
Cvičenia: pondelok 11.30 2h, F2-T3
Konzultácie: 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 (výsledky)
• 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 (výsledky)
• zobraz modul Ex03a - zoznamy
• zobraz modul Ex03b - triedenie zoznamov
• zobraz modul Ex03c - kombinatorické funkcie na zoznamoch
• 4. cvičenie (výsledky)
• zobraz modul Ex04a - binárne stromy
• zobraz modul Ex04b - binárne vyhľadávacie stromy
• 5. cvičenie (výsledky)
• zobraz modul Ex05 - symbolické výrazy a numerické termy
• 6. cvičenie (výsledky)
• zobraz modul Ex06a - výroková logika
• zobraz modul Ex06b - výrokovo-logické vyplývanie
• 7. cvičenie (výsledky)
• zobraz modul Ex07a - logická platnosť a logické vyplývanie
• zobraz modul Ex07b - verifikácia programov: explicitné definície
• 8. cvičenie (výsledky)
• 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 (výsledky)
• 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 (výsledky)
• zobraz modul Ex10 - verifikácia programov: binárne stromy
• 11. cvičenie (výsledky)
• zobraz modul Ex11 - verifikácia programov: symbolické výrazy a numerické termy
• 12. cvičenie (výsledky)
• 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