Rückblick - swl.htwsaar.de · § Für unser RAM-Programmbedeutet dies, dass unsere Invariantenach...

32

Rückblick§ RAM als einfaches Rechnermodell mit kleinem

Befehlssatz, welches wahlfrei auf seinenSpeicher zugreifen und alles berechnen kann

§ Laufzeit eines Programms für eine bestimmte Eingabewird gemessen als die Zahl der ausgeführten Befehle

Informatik 1 / Kapitel 3: RAM als Rechnermodell

33

Berechnen von x2 + y2

§ Wir schreiben nun ein RAM-Programm, welches die Eingabe x und y in s[0] und s[1]erwartet und den Wert x2 + y2 berechnet und diesen als Ausgabe in s[2] ablegt


34

3.2 Korrektheit von Programmen§ Wie können wir sicherstellen, dass ein RAM-Programm

wirklich tut, was es tun soll?

§ Man kann die Korrektheit von (zumindest einfachen)RAM-Programmen formal beweisen

§ Dazu greifen wir auf das Beweisverfahren der vollständigen Induktion zurück(vgl. Mathematik 1)


35

Vollständige Induktion§ Unser Ziel ist es zu beweisen, dass eine Aussage Ai

für beliebige Werte von i gültig ist

§ Induktionsanfang (meist für i = 1) zeigt, dass die Aussage Ai für einen initialen Wert von i gültig ist

§ Induktionsschritt (i ⇒ i+1) zeigt, dass die Aussage Ai+1

gültig ist, wenn die Aussage Ai gültig ist

§ Damit haben wir gezeigt, dass unserer Aussage Ai

für alle i > 0 gültig ist


36

Vollständige Induktion§ Beispiel: Wir wollen folgende Aussage zeigen

§ Induktionsanfang (i = 1):


i�1X

j=0

2 j = 2 i � 1

37

Vollständige Induktion§ Induktionsschritt (i⇒ i+1):


38

Berechnen von Zweierpotenzen


INPUT 0

OUTPUT 10: a <- 1

1: i1 <- s[0]2: if i1 = 0 then jump 6

3: a <- a * 24: i1 <- i1 - 1

5: jump 26: s[1] <- a

7: HALT

39

Korrektheit der Berechnung von Zweierpotenzen§ Wir möchten nun die Korrektheit unseres Programms

zum Berechnen von Zweierpotenzen beweisen

§ Zunächst beweisen wir eine Aussage Ai , welche dieSituation nach dem i-ten Schleifendurchlauf(d.h. Abarbeitung des Befehls 5) beschreibt

§ Eine solche Aussage nennt man auch Invariante,da ihre Gültigkeit beim Durchlaufen der Schleifeunverändert bleibt


a = 2i und i1 = n� i

40

Korrektheit der Berechnung von Zweierpotenzen§ Als Induktionsanfang beweisen wir nun, dass die

Aussage A1 nach dem ersten Schleifendurchlauf gilt

§ Hierzu stellen wir den Programmablauf bis nach dem ersten Schleifendurchlauf mittels einer Tabelle dar


41

Korrektheit der Berechnung von Zweierpotenzen§ Programmablauf bis nach dem ersten Schleifendurchlauf

(d.h. Abarbeitung des Befehls 5)

§ Somit gilt die Aussage A1


IP a i1 s[0] s[1]

INIT undef undef n undef0 11 n23 24 n� 15

21 n� 1

42

Korrektheit der Berechnung von Zweierpotenzen

§ Für den Induktionsschritt müssen wir beweisen, dass dieAussage Ai+1 gilt, wenn die Aussage Ai gilt

§ Für unser RAM-Programm bedeutet dies, dass unsereInvariante nach einem weiteren Schleifendurchlauf

weiterhin gilt, wenn sie zu Beginn gegolten hat

§ Wir stellen die Wertveränderungen während eines Schleifendurchlaufs in einer Tabelle dar


43

Korrektheit der Berechnung von Zweierpotenzen§ Wertveränderungen bei einem weiteren Durchlauf der

Schleife, dargestellt als Tabelle


IP a i1 s[0] s[1]

2i n� i23 2i · 24 (n� i)� 15

2i+1 n� (i+ 1)

44

Korrektheit der Berechnung von Zweierpotenzen§ Um die Korrektheit unseres gesamten RAM-Programmes

zu beweisen, müssen wir zeigen, dass beim Erreichendes Befehls 7 das korrekte Ergebnis 2n in s[1] steht

§ Unsere Schleife bricht nach i = n Durchläufen ab,wenn i1 = 0 gilt und es gilt laut unserer Invariante

d.h. im Akkumulator steht der korrekte Wert 2n

§ Es folgt der Befehl 6, wobei der Wert 2n

nach s[1] geschrieben wirdInformatik 1 / Kapitel 3: RAM als Rechnermodell

a = 2i und i1 = n� i

45

Berechnen der Fakultät§ Wir schreiben nun ein RAM-Programm, welches zu einen

in s[0] gegebenen Wert n ≥ 1 seine Fakultät n! berechnet

§ Die Fakultät ist, zur Erinnerung, wie folgt definiert


n! =nY

i=1

i = 1 · . . . · n

46

Berechnen der Fakultät


INPUT 0

OUTPUT 10: a <- 1

1: i1 <- s[0]2: i2 <- 0

3: if i1 = 0 then jump 94: i2 <- i2 + 1

5: s[2] <- i26: a <- a * s[2]

7: i1 <- i1 – 18: jump 3

9: s[1] <- a10: HALT

47

Korrektheit der Berechnung der Fakultät§ Als Induktionsanfang beweisen wir, dass folgende

Aussage Ai nach dem ersten Schleifendurchlauf(d.h. Abarbeitung des Befehls 8) gilt

§ Für den Induktionsschritt müssen wir beweisen, dass dieAussage Ai+1 gilt, wenn die Aussage Ai gilt


a = i! und i1 = n� i und i2 = i

48

Korrektheit der Berechnung der Fakultät§ Programmablauf bis nach dem ersten Schleifendurchlauf

(d.h. Abarbeitung des Befehls 8)


IP a i1 i2 s[0] s[1] s[2]

INIT undef undef undef n undef undef012345678

49

Korrektheit der Berechnung der Fakultät§ Wertveränderungen bei einem weiteren Durchlauf der

Schleife, dargestellt als Tabelle


IP a i1 i2 s[0] s[1] s[2]

i! n� i i345678

50

Korrektheit der Berechnung der Fakultät§ Unsere Schleife bricht nach n Durchläufen ab

und im Akkumulator steht der Wert n!

§ Es folgt der Befehl 9, wobei der Wert im Akkumulatornach s[1] geschrieben wird


51

Zusammenfassung§ Die Korrektheit (einfacher) RAM-Programme lässt sich

mittels vollständiger Induktion beweisen

§ Wir beweisen hierzu eine Invariante, welche nachjedem Durchlauf der Schleife gelten muss

§ Zum Beweisen des Induktionsanfangs und des Induktionsschrittes stellen wir eine Tabelle auf,welche die Wertveränderungen währenddes Programmablaufs erfasst


52

Literatur[1] H.-P. Gumm und M. Sommer: Einführung in die

Informatik, Oldenbourg Verlag, 2012 (Kapitel 5.2)


Rückblick - swl.htwsaar.de · § Für unser RAM-Programmbedeutet dies, dass unsere Invariantenach...

Documents

Transcript of Rückblick - swl.htwsaar.de · § Für unser RAM-Programmbedeutet dies, dass unsere Invariantenach...