Behörighetskrav

Kandidatexamen som innehåller Programmeringsmetodik DV1, Algebra DV1, Logik och Bevisteknik DV1, Algoritmer och datastrukturer DV1, Programmeringsteori (eller motsvarande kurser). Semantik och principer för programmeringsspråk DV1 rekommenderas.

Mål

För godkänt betyg ska studenten kunna

• förstå hur formella metoder passar in i mjukvaruutvecklingsprocessen,
• redogöra för principerna bakom modellbaserad specifikation och förfiningsbaserad programutveckling,
• redogöra för B-metoden eller annan använd metod,
• förstå och självständigt skriva modellbaserade formella specifikationer,
• självständigt utföra formell utveckling av program med verktygsstöd.

Innehåll

Översikt över specifikationsmetoder. Modellbaserad specifikation. Specifikationsspråket B eller liknande notation. Programutvecklingsprocessen. Verifiering och validering. Simulering och andra metoder för validering av specifikationer. Modeller av implementeringar. Översikt över axiomatisk semantik. Invarianter. Svagaste förvillkor. Verifiering genom förfining. B-metoden eller liknande metod. Bevisåtaganden. Bevistekniker. Verktyg för formell programutveckling.

Undervisning

Föreläsningar och seminarier. Under kursen utför studenterna ett programutvecklingsprojekt med konstruktion av formell specifikation och utveckling av bevisat korrekt programkod.

Examination

Seminarier (3 hp) och projekt (4,5 hp).