Ugeseddel 9

Bemærk: Alle studerende, også under Åben Uddannelse, skal selv tilmelde sig til eksamen. For sommereksamen sker det i uge 14, dvs. fra 29/3 til 4/4, og det foregår online på http://www.au.dk/da/studerende/ under punktet "selvbetjening".

Forelæsning 17/3

Algoritmer som transitionssystemer.

Læsning

Hansen og Schmidt, kapitel 2.

Kommentarer

Et transitionssystem anskuer en dynamisk proces som en sekvens af tilstande, hvor de mulige skift mellem tilstande kan beskrives formelt. Specielt kan algoritmer ses som transistionsystemer, hvis en tilstand defineres som værdierne af de i algoritmen indgående variable samt hvor i programmet vi er.

Formålet med at anskue algoritmer som transitionsystemer er, at man derved kan argumentere formelt om gyldighed (at algoritmen ender i den ønskede tilstand, såfremt den stopper) og terminering (at den faktisk stopper). En algoritme siges at være korrekt, hvis den for alle input som overholder inputbetingelsen er gyldig og terminerer.

I det centrale kapitel 2 i noterne defineres en minimal pseudokode, som bruges til at beskrive algoritmer. For at argumentere for korrekthed dekoreres denne pseudokode med logiske udsagn. En konkret udførsel af algoritmen kan nu ses som en kæde af skiftende udsagn og pseudekode-stumper. Vores opgave i forbindelse med gyldighed er at bevise, at hvis første udsagn (om input til algoritmen) er opfyldt, så vil enhver sådan kæde ende med at opfylde udsagnet indeholdt i outputkravet for algoritmen. Denne opgave løses ved at argumenterer for korrektheden af en relevant mængde led i kæden, alle af typen {U}sekvens-af-tildelinger{W}, hvor U og W er logiske udsagn. Et sådant led er korrekt, hvis det gælder, at hver gang man udfører de angivne tildelinger i en tilstand som opfylder U, vil det resultere i en tilstand som opfylder W. De relevante led for en given algoritme findes ved at følge opdelingsprincippet beskrevet på side 37 i noterne. Sådanne led kaldes bevisbyrder. Vores opgave i forbindelse med terminering er at finde et udtryk (mere præcist en funktion af tilstanden) som er et helt ikke-negativt tal, og som mindskes for enhver iteration af en i algoritmen indgående løkke (jf. afsnit 6.3).

Bemærk at opgaver af denne type er ofte forekommende i eksamenssæt.

Forelæsning 24/3 (forventet indhold)

Flere eksempler på algoritmer som transitionssystemer. Start på grafer.

Læsning

Hansen og Schmidt, kapitel 3.

Goodrich og Tamassia, start på kapitel 6.

Øvelser 24/3

Der er ingen øvelser i denne uge.