1-AIN-470 Špecifikácia a verifikácia programov LS 2019/20

Prednášky: utorok 08:10-9:40, m. M-IV
Cvičenia: utorok 11:30-13:00, m. I-H6
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 bol test
• 6. cvičenie (výsledky)
• zobraz modul Ex06 - symbolické výrazy a numerické termy
• 7. cvičenie (výsledky)
• zobraz modul Ex07a - primitívne rekurzívne funkcie
• zobraz modul Ex07b - univerzálna funkcia pre primitívne rekurzívne funkcie
• 8. cvičenie (výsledky)
• zobraz modul Ex08 - aritmetizácia výpočtového modelu pre čiastočne rekurzívne funkcie
• 9. cvičenie (výsledky)
• zobraz modul Ex09a - výroková logika
• zobraz modul Ex09b - výrokovo-logické vyplývanie
• 10. cvičenie (výsledky)
• zobraz modul Ex10a - logická platnosť a logické vyplývanie
• zobraz modul Ex10b - verifikácia programov: explicitné definície
• 11. cvičenie (výsledky)
• zobraz modul Ex11a - verifikácia programov: primitívna rekurzia
• zobraz modul Ex11b - verifikácia programov: 'course-of-values' rekurzia
• zobraz modul Ex11c - verifikácia programov: rekurzia s mierou
• zobraz modul Ex11d - verifikácia programov: iteratívna rekurzia
• 12. cvičenie (výsledky)
• zobraz modul Ex12a - verifikácia programov: zoznamy
• zobraz modul Ex12b - verifikácia programov: operácie na zoznamoch
• zobraz modul Ex12c - verifikácia programov: triedenie zoznamov
• 13. cvičenie (výsledky)
• zobraz modul Ex13 - verifikácia programov: binárne stromy

Hodnotenie

Tu sa nachádza súbor obsahujúci celkové 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.

Staršie správy