Kood: ITT9031
Punkte: 4.0 AP (6.0 EAP)
Nädalatunde: 4, sh loenguid 3, harjutusi 1
Kontrollivorm: eksam
Eksamihinde saamiseks tuleb semestri jooksul esitada lahendused kolmele koduülesannete komplektile (alternatiivselt kolmanda koduülesannete komplekti asemel ettekanne).
Õppejõud: prof Tarmo Uustalu, arvutiteaduse instituut, dr Keiko Nakata, Küberneetika Instituut
Kontakt: firstname(at)cs.ioc.ee, 620 4250
Tunniplaan: loengud/harjutused E 17.45-21.00 Küberneetika Majas ruum B101.
Esimene kohtumine toimus E 1.2.2010.
Konsultatsioon E 31.5.2010 kl 17.45 KübI B101.
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 1.2. | L1 | Semantika kirjeldamise meetodid, näitekeel While, avaldiste semantika | Ch 1 |
E 8.2. | L2 | Loomulik semantika | Ch 2.1 |
E 15.2. | L3 | SOS, loomuliku semantika ja SOSi samaväärsus | Ch 2.2, 2.3 |
E 22.2. | L4 | While'i laiendused, blokid ja protseduurid | Ch 2.4, 2.5 |
E 1.3. | EI TOIMU (EWSCS 2010) | ||
E 8.3. | L5 | Masinkood, kompilaator, kompilaatori korrektsus | Ch 3.1-3.3 |
E 15.3. | L6 | Otsestiili denotatsioonsemantika (spetsifikatsioon) | Ch 4.1 |
E 22.3. | EI TOIMU, LÜKKUB EDASI (24.5.) | ||
E 29.3. | L7 | Püsipunktiteooria | Ch 4.2 |
E 5.4. | L8 | Püsipunktiteooria jätk | Ch 4.2 |
E 12.4. | L9 | Otsestiili denotatsioonsemantika (konstruktsioon), denot-semantika ja operatsioonsemantika samaväärsus | Ch 4.3, 4.4 |
E 19.4. | L10 | Otsestiili denotatsioonsemantika While'i laienduste, blokkide, protseduuride jaoks | Ch 4.5 |
E 26.4. | L11 | Jätkuedastussemantika | Ch 4.5 ja lisamat |
E 3.5. | L12 | Programmianalüüs | Ch 5 või altenat mat |
E 10.5. | L13 | Programmide korrektsus, osalise korrektsuse Hoare'i loogika | Ch 6.1, 6.2 |
E 17.5. | L14 | Korrektsus ja täielikkus | Ch 6.3 |
E 24.5 | L15 | Variatsioonid (täieliku korrektsuse Hoare'i loogika jms) | Ch 6.4 |