Programmikeelte semantika (kevad 2003)

---

Registreerumine: Kursusele registreerumiseks deklarareerida selle kuulamine vastavalt kehtivale korrale dekanaadis, kuid saata ka meil Tarmo Uustalule. Tähtaeg: 17.2.2003.

---

Kood: ITT9030

Punkte: 6.0

Nädalatunde: 4, sh loenguid 3, harjutusi 1

Kontrollivorm: eksam

Eksamihinde saamiseks tuleb semestri jooksul esitada lahendused kolmele koduülesannete komplektile.

Õppejõud: dots Tarmo Uustalu, arvutiteaduse instituut

Kontakt: firstname(at)cs.ioc.ee, (0) 620 4250

Tunniplaan: loengud/harjutused R 14.00-16.30 Küberneetika Majas ruum B216 al R 7.2.2003 (mõned peavad eri põhjustel ära jääma ja tuleb järele teha teistel päevadel)

---

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: A Formal Introduction. J. Wiley & Sons, 1992.

Selle läbimüüdud raamatu parandatud versioon a-st 1999 on veebist ps-vormingus vabalt kättesaadav siit ning õppimiseks tasuta kasutatav.

V. Vene kevadel 2000 TÜs peetud sarnase kursuse koduleht on siin.

Loengute, harjutuste teemad

Kuupäev	L/H	Teema	Rmt jaotised
R 7.2.	L1	Semantika kirjeldamise meetodid, näitekeel While	Sec. 1.1-1.2
R 14.2.	L2	Avaldiste semantika, käskude loomulik semantika	Sec. 1.3, 1.4, 2.1.
R 21.2.	L3	Struktuurne operatsioonsemantika, While'i laiendused	Sec. 2.2-2.4
R 28.2.	L4	Blokkide ja protseduuride loomulik semantika	Sec. 2.5
T 11.3.	L5	Abstraktne masin ja tema SOS, koodi genereerimine, realisatsiooni korrektsus	Sec. 3.1-3.4
T 1.4.	L6	Otsestiili denotatsioonsemantika (spetsifikatsioon)	Sec. 4.1.
R 4.4.	L7	Püsipunktiteooria	Sec. 4.2.
E 14.4.	L8	Püsipunktiteooria (jätk)	Sec. 4.2
R 18.4.		Suur Reede
E 21.4.	L9	Otsestiili denotatsioonsemantika (konstruktsioon)	Sec. 4.3.
R 25.4.	L10	Otsestiili denot-semantika ja SOSi ekvivalentsus, otsestiili denot-semantika blokkide ja protseduuride jaoks	Sec. 4.4., 4.5
E 5.5.	L11	Otsestiili denot-semantika blokkide ja protseduuride jaoks (jätk)	Sec. 4.5
R 9.5	L12	Jätkuedastusstiili denotatsioonsemantika	Sec. 4.5
E 12.5.	L13	Märgianalüüs	FN61, Sec. 2.1-2.4
R 16.5.	L14	Kordamine püsipunktiteooria ja jätkuedastusstiili teemal
R 23.5.	L15	While'i, Exc'i ja Proc'i denot-semantika Haskellis

Koduülesanded

• Koduülesanded 1 (tähtaeg 1.4., pikend. 11.4.): ps.gz, pdf
• Koduülesanded 2 (tähtaeg 9.5., pikend. 16.5.): ps.gz, pdf
• Koduülesanded 3 (tähtaeg 6.6., pikend. 13.6.): ps.gz, pdf

Semantika Haskellis

• Haskell home page
• Denotatsioonsemantika Haskellis: sem-while.hs - sem-exc.hs - sem-proc.hs

Suvekoole 2003

• 8th Estonian Winter School in Computer Science, EWSCS'03 (Palmse, 2-7 March 2003)
• Summer School on the Foundation of Security, (Eugene, OR, 16-27 June 2003)
• Int. Winter School on Semantics and Applications, WSSA 2003 (Montevideo, 21-31 July 2003)
• Marktoberdorf Summer School 2003: Proof Technology and Computation (Marktoberdorf, 29 July-10 Aug. 2003)
• 15th European Summer School in Logic, Language and Information, ESSLLI 2003 (Vienna, 18-29 Aug.2003)
• 3rd Int. Summer School on Formal Methods for the Design of Computer, Commun. and Software Systems: Software Architecture, SFM-03:SA (Bertinoro, 22-27 Sept. 2003)

---

Tarmo Uustalu
Viimane uuendus 25.5.2003