Umiestnenie: ŠVP | Výučba | CL Homepage | KAI | FMFI UK v Bratislave

Súvisiace: Download | ŠVP leto 2007/08 | ŠVP leto 2008/09 | ŠVP leto 2009/10 | ŠVP leto 2010/11 | ŠVP leto 2011/12 | ŠVP leto 2012/13 | ŠVP leto 2013/14

English version

1-AIN-470 Špecifikácia a verifikácia programov LS 2014/15

Prednášky: utorok 14:50-16:20, m. M-II
Cvičenia: utorok 16:30-18:00, m. I-H3
Konzultácie: streda 13:00-13:30, m. I-16
Učiteľ: Ján Komara

Novinky

6.5.2015 Na riadne termíny sa zapisujte cez AIS2. Požiadavka: splnenie podmienok priebežného semestrálneho hodnotenia (aspoň 30 bodov podľa AIS2).

6.5.2015 priebežne aktualizované. Termíny testov a konzultácii počas skúšobného obdobia.

... tu nájdete ostatné správy.

O kurze

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

Literatúra

J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001. (PostScript) (Adobe Acrobat Document)

Cvičenia

1. cvičenie

zobraz modul Ex01a - začíname s CL
zobraz modul Ex01b - výroková logika
zobraz modul Ex01c - výrokovo-logické vyplývanie

2. cvičenie

zobraz modul Ex02a - logická platnosť
zobraz modul Ex02b - logické vyplývanie
zobraz modul Ex02c - len pre húževnatých

3. cvičenie

zobraz modul Ex03a - explicitné definície
zobraz modul Ex03b - explicitné definície

4. cvičenie

zobraz modul Ex04a - primitívna rekurzia
zobraz modul Ex04b - 'course-of-values' rekurzia

5. cvičenie

zobraz modul Ex05a - rekurzia s mierou
zobraz modul Ex05b - chvostová rekurzia a iterácia

6. cvičenie

zobraz modul Ex06a - Cantorova párovacia funkcia a aritmetizácia karteziánskeho súčinu
zobraz modul Ex06b - Catalanova párovacia funkcia

7. cvičenie

zobraz modul Ex07a - zoznamy
zobraz modul Ex07b - operácie na zoznamoch

8. cvičenie

zobraz modul Ex08 - binárne stromy

9. cvičenie

zobraz modul Ex09a - Braunove stromy a flexibilné polia
zobraz modul Ex09b - haldy a prioritné fronty

10. cvičenie

zobraz modul Ex10 - symbolické výrazy a numerické termy

11. cvičenie

zobraz modul Ex11a - triedenie zoznamov
zobraz modul Ex11b - binárne vyhľadávacie stromy

12. cvičenie

zobraz modul Ex12 - výroková logika a rozpoznávanie tautológií

Testy

1. test (zadanie) (riešenia) (výsledky)
2. test (zadanie) (riešenia) (výsledky)
opravný semestrálny test (zadanie) (riešenia) (výsledky)

Prémiové úlohy

Hodnotia sa aj čiastočne vyriešené úlohy (vysvetlenie bolo na poslednej prednáške). Úloh je päť. Viac ich nebude.

1. prémiová úloha (zadanie)

zobraz modul Ul01

2. prémiová úloha (zadanie)

zobraz modul Ul02

3. prémiová úloha (zadanie)

zobraz modul Ul03

4. prémiová úloha (zadanie)

zobraz modul Ul04

5. prémiová úloha (zadanie)

zobraz modul Ul05

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

27.5.2014 Testy sú opravené.

14.5.2015 Pridaný súbor obsahujúci celkové hodnotenie

14.5.2015 2. test je opravený.

27.4.2015 Termín 2. testu: utorok 12.5.2015 v čase 16:30-18:00 v m. I-H3.

7.4.2015 1. test je opravený.

31.3.2015 Konzultácie k 6. cvičeniu: streda 8.4.2015 v čase 14:50-18:00 v m. I-H6.

18.3.2015 Termín 1. testu: utorok 31.3.2015 v čase 16:30-18:00 v m. I-H3.

9.3.2015 Vydali sme novú verziu CL 5.81.21, ktorá funguje s aktuálnou verziou 36 prehliadača Firefox. Pre použitie na svojom vlastnom počítači s OS Windows alebo Linux si prevezmite inštalátor. Vo fakultných počítačových miestnostiach nainštalujte alebo aktualizujte CL spustením Start > Applications > Programming > CL install.

16.2.2015 Pre chorobu sa výučba predmetu začne prednáškou v utorok 24. februára 2015.

* – aktualizované v priebehu posledných 7 dní

Posledná zmena: 2015-06-03T15:04+0200