Kood: ITT9030
Punkte: 6.0
Nädalatunde: 4, sh loenguid 3, harjutusi 1
Kontrollivorm: eksam
Eksamihinde saamiseks tuleb semestri jooksul esitada lahendused kolmele koduülesannete komplektile.
Õppejõud: prof Tarmo Uustalu, arvutiteaduse instituut
Kontakt: firstname(at)cs.ioc.ee, 620 4250
Tunniplaan: loengud/harjutused R 15.30-18.00 Küberneetika Majas ruum B101 (mõned peavad eri põhjustel ära jääma ja tuleb järele teha teistel päevadel).
Esimene kohtumine toimus R 27.1.2006 kl 14.00-16.30. Edaspidi toimuvad loengud/harjutused reedeti 15.30-18.00. (Mõnel puhul ka neljapäeval 16.00-18.30.)
Aine sisu:
Programmikeelte semantika kirjeldamise meetodid, näitekeel While. Operatsioonsemantika (kahes variandis: loomulik semantika ja struktuurne operatsioonsemantika). Denotatsioonsemantika. Aksiomaatiline semantika. Rakendused: kompilaatori korrektsuse tõestamine, programmianalüüsi korrektsuse tõestamine, programmide verifitseerimine.
Õpik:
H. R. Nielson, F. Nielson. Semantics with Applications: A Formal Introduction. J. Wiley & Sons, 1992.
Selle läbimüüdud raamatu parandatud versioon a-st 1999 on ps-vormingus vabalt kättesaadav (ps.gz) ning õppimiseks tasuta kasutatav.
Ilmumas on uuem version.
Vt ka:
H. R. Nielson, F. Nielson. Semantics with Applications: Model-Based Program Analysis. DAIMI note FN61, 1996. (ps.gz). (Asendab rmt Ch 5.)
| Kuupäev | L/H | Teema | Rmt jaotised |
|---|---|---|---|
| R 27.1. | L1 | Semantika kirjeldamise meetodid, näitekeel While, avaldiste semantika | Ch 1 |
| R 3.2. | EI TOIMU (Teooriapäevad Kokel3) | ||
| R 10.2. | L2 | Loomulik semantika | Sec. 2.1. |
| R 17.2. | L3 | Struktuurne operatsioonsemantika
T Altenkirch: Functional quantum programming (slides in pdf) |
Sec. 2.2. |
| R 24.2. | Vabariigi aastapäev | ||
| R 3.3. | L4 | Loomuliku ja struktuurse operatsioonsemantika samaväärsus, While'i mitmesuguste laienduste semantika | Sec. 2.3-2.4 |
| R 10.3. | EI TOIMU (XI Eesti Arvutiteaduse Talvekool) | ||
| R 17.3. | L5 | Blokkide ja protseduuride loomulik semantika | Sec. 2.5 |
| N 23.3. | L6 | Abstraktne masin ja tema SOS, koodi genereerimine, realisatsiooni korrektsus | Sec. 3.1-3.3 |
| R 31.3. | EI TOIMU | ||
| N 6.4. | L7 | Otsestiili denotatsioonsemantika (spetsifikatsioon) | Sec 4.1 |
| R 7.4. | L8 | Püsipunktiteooria, otsestiili denotatsioonsemantika Haskellis | Sec 4.2 |
| N 13.4. | L9 | Püsipunktiteooria (jätk) | Sec 4.2 |
| R 14.4. | Suur Reede | ||
| R 21.4. | EI TOIMU | ||
| N 27.4. | L10 | Otsestiili semantika (konstruktsioon) | Sec 4.3 |
| R 28.4. | L11 | Otsestiili denot-semantika blokkide ja protseduuride jaoks | Sec 4.5 |
| N 4.5. | L12 | Jätkuedastusstiili denotatsioonsemantika, erandite denotatsioonsemantika | Sec 4.5 |
| R 5.5. | L13 | Märgianalüüs | FN 61 |
| N 11.5. | L14 | Märgianalüüs (jätk), interaktiivse väljundi denotatsioonsemantika | FN 61 |
| R 12.5. | EI TOIMU (IKT doktorikooli I aastakonverents) |