Mål:
Att studera formella metoder för systematisk utveckling och verifiering av programvara, speciellt metoder baserade på axiomatisk semantik.
Förkunskaper
TATM 43 Grundläggande diskret matematik.
TDDA 15 Logik grundkurs.
Organisation:
Föreläsningar och lektioner.
Kursinnehåll:
Axiomatisk semantik. Programkorrekthet (partiell, total). Predikatlogik. Pre- och Post-villkor. Predikattransformatorer. Målstyrd programmering. Invarianter och gränsfunktioner. Ett antal exempel.
Kurslitteratur:
Meddelas senare.
Examination:
UPG 1 Inlämningsuppgifter samt studentpresentationer.