Kood: ITT8030
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 R 8-11.30 ICT-A2.
Esimene kohtumine toimus R 7.2.2014.
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 |
---|---|---|---|
R 7.2. | L1 | Semantika kirjeldamise meetodid, näitekeel While, avaldiste semantika | Ch 1 |
R 14.2. | L2 | Loomulik semantika | Ch 2.1 |
R 21.2. | L3 | SOS big-small.hs - big-print.hs - big-assignexp.hs |
Ch 2.2 |
R 28.2. | L4 | Loomuliku semantika ja SOSi samaväärsus, While'i laiendused big-small-nondet-par.hs |
Ch 2.3, 2.4 |
R 7.3. | EI TOIMU (EWSCS 2014) | ||
R 14.3. | ÜLE VIIDUD N 3.4. | ||
R 21.3. | L5 | Blokid ja protseduurid big-proc.hs |
Ch 2.5 |
R 28.3. | L6 | Masinkood, kompilaator, kompilaatori korrektsus machine.hs - machine-better.hs |
Ch 3.1-3.3 |
N 3.4. | L7 | Otsestiili denotatsioonsemantika (spetsifikatsioon), püsipunktiteooria denot.hs |
Ch 4.1, 4.2 |
R 4.4. | L8 | Püsipunktiteooria jätk | Ch 4.2 |
R 14.3. | ÜLE VIIDUD N 17.4. | ||
N 17.4. | L9 | Otsestiili denotatsioonsemantika (konstruktsioon), denot-semantika ja operatsioonsemantika samaväärsus | Ch 4.3, 4.4 |
R 7.3. | SUUR REEDE | ||
R 25.4. | L10 | Otsestiili denotatsioonsemantika While'i laienduste, blokkide, protseduuride jaoks | Ch 4.5 |
R 2.5. | L11 | Jätkuedastussemantika contin.hs - exc.hs |
Ch 4.5 |
R 9.5. | L12 | Jätkuedastussemantika (jätk), programmianalüüs | Ch. 4.5, FN61 |
R 16.5. | L13 | Programmide korrektsus, osalise korrektsuse Hoare'i loogika | Ch 6.1, 6.2 |
R 23.5. | L14 | Korrektsus ja täielikkus, variatsioonid | Ch 6.3, 6.4 |