De studerende lærer at forstå og anvende de centrale modeller der
bliver introduceret i løbet af kurset og at bruge teknikker
relateret til disse formalismer.
Læringsmål:
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
fortolke betydningen af en given beskrivelse i en formel model
(f.eks. semantikker)
udlede en beskrivelse i en formel model (f.eks. semantikker,
inference systemer) for en ønsket egenskab eller opførsel givet som
en tekstuel beskrivelse
ændre en given beskrivelse svarende til et givet kriterie
(f.eks. tilføjelse af sprogkonstruktioner)
afgøre om en beskrivelse i en formel model opfylder en givet
egenskab
udlede en egenskab ved at anvende bevisstrategier (f.eks.
strukturel induktion, givne sætninger)
vælge formelle modeller der kan være nødvendige eller nyttige
ved løsning af et givent problem
opnå målene som del af en gruppe, mens det individuelle ansvar
opretholdes
kommunikere sine konstruktioner og løsninger på en klar og
præcis måde
Kursusindhold:
Transitionssystemer, deres brug i operationel semantik for
forskellige programmeringsparadigmer, samt formelle teknikker til
at sammenligne specifikationer.
Inferenssystemer og deres anvendelser inden for simple type
systemer og simple sikkerhedsegenskaber.
Litteraturhenvisninger:
- Semantics With Applications - An Appetizer, Hanne Riis Nielson
and Flemming Nielson, Springer 2007.
Bemærkninger:
Kursets indhold er identisk med den sidste del af kurset 02141
"Datalogisk Modellering." Kurset begynder omkring midten
af marts og samlæses med kursus 02141.
