FDD3457 Programsemantik och programanalys 6,0 hp
Denna kurs är avvecklad.
Sista planerade examination: HT 2023
Avvecklingsbeslut:
Ingen information tillagd
Att ge en semantik för ett programspråk betyder att ge en exakt definition av programbeteendet för program skrivna på detta språk. När språkets semantik har beskrivits formellt, kan man börja och bevisa olika programspråkegenskaper, bevisa korrektheten av programimplementeringar baserade på abstrakta maskiner, motivera olika programanalyser som används i syntaxorienterade redaktörer och programtransformationer som används i optimerande kompilatorer, och specificera och bevisa korrektheten hos konkreta program. Detta ger den formella grunden för ett antal olika programverktyg för programanalys, optimering och verifikation.
Innehåll och lärandemål
Kursinnehåll
Del I. Operationell semantik och språkimplementering: naturlig semantik, strukturell operationell semantik, abstrakta maskiner, korrekt implementering av språk.
Del II. Denotationell semantik and programanalys: denotationell semantik, fixtpunktteori, programanalys och transformation.
Del III. Axiomatisk semantik and programverifikation: axiomatisk semantik, programspecifikation och verifikation, svagaste förutsättningar, generering av verifieringsvillkor.
Lärandemål
Efter avslutad kurs ska den framgångsrika doktoranden kunna:
- Redogöra för de huvudsakliga semantiska stilarna som används för att fånga programmens mening på ett formellt sätt, både i teori och på exempel.
- Relatera de olika semantiska stilarna och jämföra deras styrkor och svagheter.
- Använda dessa semantiska stilar för programanalys, optimering och verifiering, både i teorin och som en grund för mjukvaruverktyg.
- Utöka ett programmeringsspråk med nya språkfunktioner, och förlänga dess semantik i enlighet därmed.
- Bevisa formella egenskaper hos en given semantik.
Kurslitteratur och förberedelser
Särskild behörighet
Rekommenderade förkunskaper
Utrustning
Kurslitteratur
Nielson and Nielson "Semantics with Applications: An Appetizer", Springer-Verlag, 2007, ISBN: 978-1-84628-691-9. Research papers.
Examination och slutförande
När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.
Betygsskala
Examination
- EXA1 - Examination, 6,0 hp, betygsskala: P, F
Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.
Examinator får medge annan examinationsform vid omexamination av enstaka studenter.
Övriga krav för slutbetyg
För att klara kursen måste doktorander bli godkända på hemtalen, laborationsuppgifterna, seminariet och den skriftliga tentamen.
Möjlighet till komplettering
Möjlighet till plussning
Examinator
Etiskt förhållningssätt
- Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
- Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
- Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.