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