Hoppa till huvudinnehållet
Till KTH:s startsida Till KTH:s startsida

DD2557 Programsemantik och programanalys 7,5 hp

Administrera Om kursen

Att ge en semantik för ett programspråk innebär att ge en exakt definition av beteendet hos program skrivna i detta språk. Nar väl semantiken i språket har beskrivits formellt kan man gå fram och bevisa olika språkegenskaper som determinism, bevisa korrektheten av programimplementeringar baserade på abstrakta maskiner, motivera olika programanalyser som används i syntaxorienterade editorer och programtransformationer som används för att optimera kompilatorer, och specificera och bevisa korrektheten hos konkreta program. Detta utgör den formella grunden för en mängd programvaruverktyg för programanalys, optimering och verifiering.

Välj termin och kursomgång

Välj termin och kursomgång för att se aktuell information och mer om kursen, såsom kursplan, studieperiod och anmälningsinformation.

Kursval

Gäller för kursomgång

VT 2025 semant25 programstuderande

Anmälningskod

60440

Rubriker med innehåll från kursplan DD2557 (VT 2023–) är markerade med en asterisk ( )

Innehåll och lärandemål

Kursinnehåll

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.

Lärandemål

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.

Kurslitteratur och förberedelser

Särskild behörighet

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.

Rekommenderade förkunskaper

Ingen information tillagd

Utrustning

Ingen information tillagd

Kurslitteratur

Ingen information tillagd

Examination och slutförande

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

Betygsskala

A, B, C, D, E, FX, F

Examination

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

Möjlighet till komplettering

Ingen information tillagd

Möjlighet till plussning

Ingen information tillagd

Examinator

Profile picture Dilian Gurov

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.

Ytterligare information

Kursrum i Canvas

Registrerade studenter hittar information för genomförande av kursen i kursrummet i Canvas. En länk till kursrummet finns under fliken Studier i Personliga menyn vid kursstart.

Ges av

EECS/Datavetenskap

Huvudområde

Datalogi och datateknik

Utbildningsnivå

Avancerad nivå

Påbyggnad

Ingen information tillagd

Övrig information

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