Behörighetskrav

120 hp med 30 hp matematik och 30 hp datavetenskap, inklusive grundläggande programmering, datastrukturer och grundläggande logik.

Mål

Efter kursen ska studenterna ha förmåga att:

- Skriva rigorösa beskrivningar av specifikation och implementering av program.

- Verifiera program, dvs. kunna bevisa att implementeringen av ett program uppfyller specifikationen av programmet

- Syntetisera program, dvs. skapa ett korrekt program från en given specifikation.

Innehåll

Kursen innehåller följande områden:

- Logiska bevis

- Specifikation av, och korrekthet hos, program

- "weakest precondition"

- Invarianter

- Partiell korrekthet

- Termineringsbevis

- Fullständig korrekthet

- Programsyntes

Undervisning

Föreläsningar och lektioner

Examination

Skriftlig tentamen och inlämningsuppgifter

Övriga föreskrifter

Kursen får ej tillgodoräknas i examen tillsammans med kursen 2AD094 Programteori.