Programmikeelte semantika (kevad 2010)


Registreerumine: Kursusele registreerumiseks deklarareerida selle kuulamine vastavalt kehtivale korrale dekanaadis, kuid samuti teatada Tarmo Uustalule oma meiliaadress. Tähtaeg: 15.2.2010.

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.


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

Koduülesanded

Semantika Haskellis

Semantilisi suvekoole 2010


Tarmo Uustalu
Viimane uuendus 25.5.2010