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.

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. L6 Masinkood, kompilaator, kompilaatori korrektsus Ch 3.1-3.3
E 15.3. L7 Otsestiili denotatsioonsemantika (spetsifikatsioon) Ch 4.1
E 22.3. L8 Püsipunktiteooria Ch 4.2
E 29.3. L9 Püsipunktiteooria jätk Ch 4.2
E 5.4. L10 Otsestiili denotatsioonsemantika (konstruktsioon), denot-semantika ja operatsioonsemantika samaväärsus Ch 4.3, 4.4
E 12.4. L11 Otsestiili denotatsioonsemantika While'i laienduste, blokkide, protseduuride jaoks Ch 4.5
E 19.4. L12 Jätkuedastussemantika Ch 4.5 ja lisamat
E 26.4. L13 Programmianalüüs Ch 5 või altenat mat
E 3.5. L14 Programmide korrektsus, osalise korrektsuse Hoare'i loogika Ch 6.1, 6.2
E 10.5. L15 Korrektsus ja täielikkus Ch 6.3
E 17.5 L16 Variatsioonid (täieliku korrektsuse Hoare'i loogika jms) Ch 6.4

Koduülesanded

Semantika Haskellis

Semantilisi suvekoole 2010

Tarmo Uustalu
Viimane uuendus 16.3.2010