Behörighetskrav

120 hp som innehåller Programkonstruktion, Algebra, Logik och Bevisteknik, Algoritmer och datastrukturer I, Programmeringsteori (eller motsvarande kurser). Engelska 6. (Med en svensk kandidatexamen uppfylls kravet på engelska.)

Mål

Efter godkänd kurs 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).

Om särskilda skäl finns får examinator göra undantag från det angivna examinationssättet och medge att en enskild student examineras på annat sätt. Särskilda skäl kan t.ex. vara besked om särskilt pedagogiskt stöd från universitetets samordnare för studenter med funktionsnedsättning.