Behörighetskrav

20 p/30 hp datavetenskap och 20 p/30 hp matematik

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 specikationen 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

- Specikation av, och korrekthet hos, program

- "weakest precondition"

- Invarianter

- Partiell korrekthet

- Termineringsbevis

- Fullständig korrekthet

- Programsyntes

Undervisning

Föreläsningar och lektioner

Examination

Det teoretiska momentet som omfattar 4,5 hp examineras med tentamen och det praktiska momentet som omfattar 3 hp examineras med uppgifter.

Övriga föreskrifter

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