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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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)

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

36

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

§ Induktionsanfang (i = 1):

Informatik 1 / Kapitel 3: RAM als Rechnermodell

i�1X

j=0

2 j = 2 i � 1

37

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

38

Berechnen von Zweierpotenzen

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

41

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

(d.h. Abarbeitung des Befehls 5)

§ Somit gilt die Aussage A1

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

43

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

Schleife, dargestellt als Tabelle

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

n! =nY

i=1

i = 1 · . . . · n

46

Berechnen der Fakultät

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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)

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

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

Informatik 1 / Kapitel 3: RAM als Rechnermodell

52

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

Informatik, Oldenbourg Verlag, 2012 (Kapitel 5.2)

Informatik 1 / Kapitel 3: RAM als Rechnermodell