DD2557 Programsemantik och programanalys 7,5 hp

Del I. Operationell semantik och språkimplementation: naturlig semantik, strukturell operationell semantik, abstrakta maskiner, korrekthet av språkimplementation.

Del II. Denotationell semantik och programanalys: denotationell semantik, fixpunktsteori, abstrakt interpretation, programanalys och programtransformation.

Del III. Axiomatisk semantik och programverifikation: axiomatisk semantik, programspecifikation och verifikation, svagaste förutsättningar, generering av verifieringsvillkor.

Efter godkänd kurs ska studenten kunna

• konstruera tillståndsrummet för ett program som en grund för programbeteendeanalys
• översätta program till abstrakt maskinkod och exekvera den
• beräkna denotationen för ett program
• utöka ett programspråk med nya språkkonstruktioner och utöka dess semantik och abstrakta maskinimplementationer i enlighet därmed
• föreslå och motivera programtransformationer som stöds av en lämplig programanalys
• specificera och verifiera program i Hoares logik
• generera verifieringsvillkor för ett givet program och specifikation
• formellt relatera olika semantiska stilar
• formellt bevisa språkegenskaper som determinism och terminering
• formellt bevisa korrektheten för en given programtransformation genom att visa ekvivalens mellan originalprogrammet och det transformerade programmet
• formellt visa egenskaper för en given semantik.

Kunskaper och färdigheter i programmering, 5 hp, motsvarande slutförd kurs DD1337/DD1310-DD1318/DD1321/DD1331/DD100N/ID1018.

Kunskaper i grundläggande datalogi, 6 hp, motsvarande slutförd kurs DD1338/DD1320-DD1327/DD2325/ID1020/ID1021.

Kunskaper i diskret matematik, 6 hp, motsvarande slutförd kurs SF1688/SF1610/SF1630/SF1662/SF1679.

När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.

• HEM1 - Hemuppgifter, 2,5 hp, betygsskala: P, F
• LAB1 - Laborationer, 2,5 hp, betygsskala: P, F
• TEN1 - Hemtentamen, 2,5 hp, betygsskala: A, B, C, D, E, FX, 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.

Dilian Gurov

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

I denna kurs tillämpas EECS hederskodex, se:
http://www.kth.se/eecs/utbildning/hederskodex