Hoppa till huvudinnehållet

DD2557 Programsemantik och programanalys 7,5 hp

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 information från rätt kursplan och kursomgång.

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.

Kursupplägg

Ingen information tillagd

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

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

Kurswebb

Ytterligare information om kursen kan hittas på kurswebben via länken nedan. Information på kurswebben kommer framöver flyttas till denna sida.

Kurswebb DD2557

Ges av

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