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