02143 Formelle sprog og semantik

2024/2025

Kursusinformation
Formal Languages and Semantics
Engelsk
5
Bachelor
F3A (tirs 8-12) og F4B (fre 8-12)
Kursusforelæsningerne finder sted tirsdage og fredage (sammen med 02141) men kun i 13 af de 26 slots. Forelæsningsplanen vil blive annonceret på DTU Learn.
Campus Lyngby
Forelæsninger, teoretiske øvelser, programmeringsøvelser og en obligatorisk opgave.
13-uger
F4B
Skriftlig eksamen og bedømmelse af opgave(r)
Skriftlig eksamen (som normalt ændres til mundtlig ved reeksaminer). Et antal individualiserede programmeringsopgaver vil indgå i den samlede vurdering.
Skriftlig eksamen: 4 timer
Alle hjælpemidler - med adgang til internettet
7-trins skala , ekstern censur
02141
(01001/01019).­02105.­(02100/02157) , Grundlæggende viden om diskret matematik (logik, mængder, grafer, funktioner, induktion) - som forudsat f.eks. i 01001 og 01019 Grundlæggende viden om algoritmer og datastrukturer - som forudsat f.eks. i 02105. Grundlæggende viden om funktionel programmering - som forudsat f.eks. i 02100 og 02157.
Alberto Lluch Lafuente , Lyngby Campus, Bygning 321, Tlf. (+45) 4525 3736 , albl@dtu.dk
01 Institut for Matematik og Computer Science
https://courses.compute.dtu.dk/02143
I studieplanlæggeren
Overordnede kursusmål
De studerende lærer at anvende centrale datalogiske modeller og formalismer, at udvikle værktøjer baseret på disse formalismer og at bruge disse værktøjer til at analysere softwarekode.
Læringsmål
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
  • anføre forskelle i udtrykskraft af de præsenterede formelle modeller;
  • tolke betydningen af en formel model (f.eks. automater, grammatiker, semantikker):
  • udlede en formel model for en ønsket egenskab eller opførsel givet som en tekstuel beskrivelse;
  • oversætte en model til en anden model (f.eks. regulære udtryk til NFA);
  • ændre en model svarende til et givet kriterie (f.eks. fjernelse af afskedigelser, fjernelse af uklarheder grammatik);
  • anvende udvalgte værktøjer til at køre programmer og udvikle ny værktøjer baseret på de formelle modeller (f.eks. compilere & tolke);
  • udlede egenskaber ved at anvende bevisstrategier (f.eks. matematisk induktion, strukturel induktion);
  • udlede egenskaber af formelle modeller ved at anvende bevisstrategier (f.eks. matematisk induktion, givne sætninger);
  • vælge formelle modeller der kan være nødvendige eller nyttige ved løsning af et givent problem;
Kursusindhold
Kurset omfatter to emner:

(1) Formelle sprog og deres brug til at beskrive syntaks. For regulære sprog behandles måder at beskrive dem med automata og regulære udtryk, deres sammehæng, praktiske anvendelser (fx søgning, leksikalsk analyse, formelle specifikationer). For kontekstfri sprog behandles måder at beskrive dem med pushdown automata og kontekstfri grammatik, en række anvendelser (fx til parsing af programmer, dokumenter og formateret data) sammen med en kort indføring til stakautomater og deres sammenhæng med kontekstfri sprog.

(2) Formelle metoder og deres brug til både modellering og analyse af IT systemers egenskaber, især software koe. Dette inkluderer semantik af programmeringssprog og deres brug til at bygge en compiler.

Kurset involverer praktisk brug af forskellige værktøjer, og de studerende skal løse både teoretiske og praktiske opgaver, som integrerer kursets to emner.

Deltagere i 02143, der ønsker at tage imod hele tilbuddet på 02141 er velkommen til at skifte til 02141 efter aftale med lærerne.

Kurset 02141 giver en dybere behandling og praktisk oplevelse af forskellige formelle sprog og formelle metoder. Især dækker 02141 centrale praktiske og teoretiske aspekter af formelle sprog (f.eks. afgørelighed af grundlæggende problemer, pumping lemma, minimering af automater). Desuden giver 02141 en dyb behandling og praktisk erfaring med metoder til at analysere programmer (programverifikation, programanalyse, informationsflowsikkerhed og modeltjek), mens 02143 kun vil give et kort overblik over de.
Litteraturhenvisninger
(1) "Introduction to Automata Theory, Languages, and Computation", af John E. Hopcroft, Rajeev Motwani, Jefrey D. Ullman, Third Edition, Addison-Wesley, 2007.
Kursusbogen "02141: Automata Theory and Languages" udvalgt af Hanne Riis Nielson indeholder de nødvendige kapitler.
(2) "Formal Methods - An Appetizer" af Flemming Nielson og Hanne Riis Nielson, Springer, 2019.
Bemærkninger
Kurset gives på engelsk.
Sidst opdateret
02. maj, 2024