Kurset har til formål at introducere deltagerne til matematisk baserede metoder til udvikling af programmelsystemer og i særdeleshed at give dem færdigheder i at konstruere og anvende formelle specifikationer under brug af forskellige abstraktions- og modelleringsteknikker.
Læringsmål:
En studerende, der fuldt ud har opfyldt kursets mål, vil kunne:
opstille en formel specifikation ud fra en uformel opgavebeskrivelse
anvende udvalgte specifikations-stile og -teknikker
trinvis forfine en specifikation
opstille verifikationsforpligtelser
verificere simple verifikationsforpligtelser
oversætte en specifikation til et udførbart program
anvende udvalgte værktøjer relateret til formelle metoder
forklare hvad der kan opnås ved brug af formelle metoder
kommunikere resultater på en klar og præcis måde
Kursusindhold:
Formel specifikation med udgangspunkt i et eller flere typiske eksempler på specifikationssprog. Forskellige specifikationsteknikker: model-orienteret versus algebraisk; applikativ versus imperativ. Trinvis udvikling og verifikation. Implementeringsrelation(er). Løsning af specifikationsopgaver under anvendelse af datamatbaserede værktøjer.
