Behörighetskrav

120 hp som innehåller Programkonstruktion, Algebra, Logik och Bevisteknik, Algoritmer och datastrukturer I, Programmeringsteori (eller motsvarande kurser).

Mål

För godkänt betyg ska studenten kunna

• använda formella metoder 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,
• 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 (7 hp).