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 anvende og skrive formelle specifikationer under brug af forskellige abstraktions- og modelleringsteknikker.
Kursusindhold:
Formel specifikation med udgangspunkt i et eller flere typiske eksempler på specifikationssprog. Indføring i forskellige specifikationsteknikker: model-orienteret versus algebraisk; applikativ versus imperativ. Trinvis udvikling og verifikation (formel bevisførelse). Implementeringsrelationer. Løsning af specifikationsopgaver under anvendelse af datamatbaserede specifikationsværktøjer.