Kood: ITT9031
Punkte: 6.0 EAP
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 E 14.30-17.30 Küberneetika Majas ruum B101.
Esimene kohtumine toimus E 30.1.2012.
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: An Appetizer. Springer, 2007. (publisher's page)
Raamatu esmatrüki (Wiley, 1992) parandatud versioon a-st 1999 on veebist vabalt kättesaadav (pdf) ning õppimiseks tasuta kasutatav.
Vt ka:
H. R. Nielson, F. Nielson. Semantics with Applications: Model-Based Program Analysis. DAIMI note FN61, 1996. (pdf). (Asendab rmt Ch 5.)
Kuupäev | L/H | Teema | Rmt jaotised |
---|---|---|---|
E 30.1. | L1 | Semantika kirjeldamise meetodid, näitekeel While, avaldiste semantika | Ch 1 |
E 6.2. | L2 | Loomulik semantika | Ch 2.1 |
E 13.2. | L3 | SOS | Ch 2.2 |
E 20.2. | L4 | Loomuliku semantika ja SOSi samaväärsus, While'i laiendused | Ch 2.3, 2.4 |
E 27.2. | EI TOIMU (EWSCS 2012) | ||
E 5.3. | L5 | Blokid ja protseduurid | Ch 2.5 |
E 12.3. | L6 | Masinkood, kompilaator, kompilaatori korrektsus | Ch 3.1-3.3 |
E 19.3. | L7 | Otsestiili denotatsioonsemantika (spetsifikatsioon), püsipunktiteooria | Ch 4.1, 4.2 |
E 26.3. | EI TOIMU, LÜKKUB EDASI (28.5.) | ||
E 2.4. | L8 | Püsipunktiteooria jätk | Ch 4.2 |
E 9.4. | L9 | Otsestiili denotatsioonsemantika (konstruktsioon), denot-semantika ja operatsioonsemantika samaväärsus | Ch 4.3, 4.4 |
E 16.4. | L10 | Otsestiili denotatsioonsemantika While'i laienduste, blokkide, protseduuride jaoks | Ch 4.5 |
E 23.4. | L11 | Jätkuedastussemantika | Ch 4.5 |
E 30.4. | L12 | Jätkuedastussemantika (jätk), programmianalüüs | Ch. 4.5, FN61 |
E 7.5. | L13 | Programmide korrektsus, osalise korrektsuse Hoare'i loogika | Ch 6.1, 6.2 |
E 14.5. | L14 | Korrektsus ja täielikkus, variatsioonid | Ch 6.3, 6.4 |
E 28.5 | L15 | Kordamine, küsimustele vastamine |