Programmikeelte semantika (kevad 2014)

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.


Mis on semantika? Semantika on kunst, kuidas fikseerida, mida ühe keele väljendid tähendavad. Programmikeelte semantika tegeleb meetoditega programmide tähenduse fikseerimiseks. Seda ala tundmata ei saa tõsiselt tegeleda kompilaatori, verifitseerija ega ühegi muu mittetriviaalsel viisil programme töötleva süsteemi ehitamisega.

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.)

Varasemaid semantikakursusi TTÜs ja TÜs

Loengute, harjutuste teemad

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

Koduülesanded

Semantika Haskellis (kevadsemester 2012)


Tarmo Uustalu
Viimane uuendus 29.5.2014