Formålet er at give de studerende en indføring i nogle basale deklarative formalismer fra formel datalogi som vil kunne anvendes til at beskrive, analysere og vurdere aspekter af eksisterende eller påtænkte IT-systemer. Dette involverer teoretisk indsigt såvel som praktiske færdigheder i relevante avancerede programmeringssprog.
Kursusindhold:
Den ene streng vil omhandle inferenssystemer og formelle logiske systemer. Som en videreudvikling af prædikat-logikken fra "Matematik og Databaser" vil første ordens logiske systemer blive introduceret og som en fortsættelse af "Datalogisk Modellering" vil der blive lagt vægt på at klargøre den udtryksmæssige styrke i inferenssystemer. Der vil være mulighed for at inddrage eksempler på temporale og modale logikker til at beskrive dynamiske egenskaber ved systemers opførsel. Der vil blive lagt særligt vægt på de fragmenter der kan udføres maskinelt, herunder Horn-klausuler, og de studerende vil få praktisk erfaring med relevante programmeringssprog som fx Prolog.
Den anden streng vil omfatte modellering ved hjælp af funktionsprogrammering og den tilhørende analyse ved hjælp af type- og effekt-systemer. Der vil her ske et tilbageblik dels til den objekt-orienterede undervisning, dels til den vekslen mellem abstraktionsniveauer som også sås i "Matematik og Databaser", og endelig til den begyndende funktionelle beskrivelse af formelle automater fra "Datalogisk Modellering". Det vil være muligt at inddrage type- og effekt- systemer hvor værdier har fysiske dimensioner (motiveret i mange ingeniørmæssige anvendelser som fx Mars Climate Orbiter) og hvor kommunikationsstrukturen modelleres. De studerende vil få praktisk erfaring med relevante programmerings- sprog som fx OCAML eller F#.
Det praktiske element understreges af at avancerede programmeringssprog som Prolog og OCAML bruges som hurtige prototyping værktøjer (ikke at forveksle med nye alt-omfattende programmeringssprog som skal opfattes som konkurrenter til sprog som Java og C#).
