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 køre og 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;
- relatere udtryksevne til begrænsninger af beregningsmodeller
(f.eks. afgørelighed/uafgørlighed af grundlæggende problemer)
- tolke betydningen af en formel model (f.eks. automater,
grammatikker, semantikker, transitionsystemer, formelle
specifikationer):
- udlede en formel model (f.eks. automater, grammatiker,
semantikker) for en ønsket egenskab eller opførsel givet 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 redundans, fjernelse af flertydighed i grammatik);
- anvende udvalgte værktøjer og udvikle nye værktøjer baseret på
de formelle modeller for at køre og analysere programmer (f.eks.
compilere, tolke, programverifikatorer, analysatorer og
modeltjekkere)
- afgøre om en beskrivelse i en formel model opfylder en givet
egenskab;
- udlede egenskaber af formelle modeller ved at anvende
bevisstrategier (f.eks. matematisk induktion, strukturel
induktion);
- udlede egenskaber af programmer ved hjælp af automatiserede
formelle metoder;
- 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) og nogle
væsentlige teoretiske resultater (fx herunder
afgørlighedsegenskaber af væsentlige problemer). 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 kode. Dette omfatter
semantik af programmeringssprog og dets brug til at bygge compilere
og tolke, såvel som deres brug som grundlag for automatiserede
metoder til at analysere programmer. Vi vil især dække
programverifikation, programanalyse, sikkerhedsanalyse og
modeltjek.
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. Til sidst dækker vi nogle
grundlæggende praktiske og teoretiske aspekter af formelle sprog
(f.eks. pumping lemma, Turing-maskiner, minimering af automater).
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. Videoer på YouTube kanalen
FormalMethodsDK. Slides og on-line systemer på
FormalMethods.dkBemærkninger
Kurset gives på engelsk.
Sidst opdateret
06. januar, 2025