Korrektheitsbeweis rekursiv Binärbaum

Bei Postings zu Aufgabe Nr. x auf Blatt Nr. y lassen Sie Ihr Betreff bitte mit "y.x: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!

Moderator: Algorithmen und Datenstrukturen

Forumsregeln
Bei Postings zu Aufgabe Nr. x auf Blatt Nr. y lassen Sie Ihr Betreff bitte mit "y.x: " beginnen, gefolgt von einer möglichst präzisen Überschrift, danke!
fy06keju
Neuling
Neuling
Beiträge: 7
Registriert: 5. Sep 2016 16:52

Korrektheitsbeweis rekursiv Binärbaum

Beitrag von fy06keju » 16. Sep 2016 18:48

Guten Tag, ich hatte an einer Programmieraufgabe vom Javaübungsblatt versucht ein Korrektheitsbeweis zu führen.
Es geht um die Aufgabe 3.5.4 numberOfNodesOnLevel für ein Binärbaum (rekursiv)
Die Methode soll also die Gesamtzahl von Knoten im Baum, die auf der gesuchten Höhenstufe ist, zurückgeben.

Ich bitte um etwas Feedback! Danke
Hier mein Code:

Code: Alles auswählen

public int numberOfNodesOnLevel(TreeNode<T> wurzel, int level) {
return numberOfNodesOnLevelHelp(wurzel, level, 0);}

public int numberOfNodesOnLevelHelp(TreeNode<T> wurzel, int level, int actlevel) {
	if(wurzel == null) return 0;
	if(actlevel == level) {
		return 1;
	else return numberOfNodesOnLevelHelp(wurzel.left, level, actlevel+1) +  numberOfNodesOnLevelHelp(wurzel.right, level, actlevel +1); }}

Korrektheitsbeweis

Input: wurzel != null, die korrekt auf die Wurzel eines Binärbaums zeigt
eine natürliche Zahl level, die die gesuchte Höhenstufe angibt, wobei 0<= level < Integer.Max.Value
eine natürliche Zahl actLevel, die die aktuelle Höhenstufe im gegebenen Baum angibt, actLevel < Integer.Max.Value

Output: Gesamtanzahl der Knoten auf der gesuchten Höhe 'level'

Wohldefiniertheit: aufgrund der Einschränkung des Inputs kein Überlauf
da wurzel != null kein NullpointerExceptions
keine Division durch Null
Variante: die Höhe des Baumes, auf die die wurzel zeigt, nimmt ab

Terminierung: aus der Variante folgt nach endlich vielen Schritten der Rekursionsabbruch

Invariante: wenn die (Teil-)Struktur mit der Wurzel 'wurzel' ein korrekt gebildeter Binärbaum ist, so liefert der Algorithmus korrekterweise die Gesamtanzahl der Knoten auf der gesuchten Höhenstufe 'level'.

Induktionsanfang: wenn wurzel == null so liefert der Algorithmus korrekterweise 0 zurück, da kein Knoten auf der Höhe 'level' existiert.

Induktionsschritt:
Fallunterscheidung:
1.wenn actlevel== level, dh. wenn die gesuchte Höhe der aktuellen Höhe entspricht, so wird 1 zurückgegeben und die Rekursiv bricht ab, sodass seine eventuell weiteren Kinder nicht mehr betrachtet werden.
2. falls die aktuelle Höhe nicht der gesuchten Höhe entspricht, so ruft sich der Algorithmus rekursiv auf. Der rekursive Aufruf erfolgt für den linken sowie den rechten Nachfolger des aktuellen Knotens.Nach der Induktionsvoraussetzung gilt, dass die beiden rekursiven Aufrufe für den linken und rechten Teilbaum der 'wurzel' korrekt sind. Dabei wird korrekterweise die aktuelle Höhe 'level' um eins inkrementiert. Schließlich werden die Ergebnisse der beiden rekursiven Aufrufe zusammen addiert, sodass am Ende korrekterweise die Gesamtanzahl der Knoten auf der gesuchten Höhe zurückgegeben wird.

Korrektheit: Aufgrund der Variante und Abbruchbedingung folgt, dass der Algorithmus nach endlich vielen Rekursionsschritten terminiert und die Invariante garantiert die Korrektheit des Ergebnisses.

Prof. Karsten Weihe
Moderator
Moderator
Beiträge: 1824
Registriert: 21. Feb 2005 16:33

Re: Korrektheitsbeweis rekursiv Binärbaum

Beitrag von Prof. Karsten Weihe » 17. Sep 2016 09:01

fy06keju hat geschrieben: Hier mein Code:
Sieht für mich auf den ersten Blick gut aus.
fy06keju hat geschrieben: Korrektheitsbeweis

Input: wurzel != null, die korrekt auf die Wurzel eines Binärbaums zeigt
Ich denke nicht, dass Sie wurzel != null hier voraussetzen können, ist auch überhaupt nicht notwendig.
fy06keju hat geschrieben: Output: Gesamtanzahl der Knoten auf der gesuchten Höhe 'level'
Ok.

Zur Klarstellung könnte man (muss aber nicht unbedingt) noch schreiben, dass die Rückgabe 0 ist, wenn diese Höhenstufe im Baum gar nicht vorkommt.
fy06keju hat geschrieben: Wohldefiniertheit: aufgrund der Einschränkung des Inputs kein Überlauf
Ja, es wären Rechnerarchitekturen denkbar, bei denen die Tiefe des Baumes > Integer.MAX_VALUE ist. Für die Klausur muss man an so einen krassen Fall natürlich nicht denken.
fy06keju hat geschrieben: Variante: die Höhe des Baumes, auf die die wurzel zeigt, nimmt ab
Ok.
fy06keju hat geschrieben: Terminierung: aus der Variante folgt nach endlich vielen Schritten der Rekursionsabbruch
Ja, reicht, da offensichtlich korrekt.
fy06keju hat geschrieben: Invariante: wenn die (Teil-)Struktur mit der Wurzel 'wurzel' ein korrekt gebildeter Binärbaum ist, so liefert der Algorithmus korrekterweise die Gesamtanzahl der Knoten auf der gesuchten Höhenstufe 'level'.
Die Voraussetzung mit dem korrekt gebildeten Baum steht ja schon bei der Spezifikation des Inputs. Es ist nicht falsch, das hier als Konditionalsatz zu wiederholen, aber potentiell verwirrend für den Leser, weil es nach einer Fallunterscheidung klingt, bei der der zweite Fall nicht erwähnt wird. (Der Leser könnte sich fragen: "ok, und wenn der Baum nicht korrekt ist?", und muss dann erst wieder zurückschauen auf die Spezifikation des Inputs.)
fy06keju hat geschrieben: Induktionsanfang: wenn wurzel == null so liefert der Algorithmus korrekterweise 0 zurück, da kein Knoten auf der Höhe 'level' existiert.
Ok.
fy06keju hat geschrieben: Induktionsschritt:
Fallunterscheidung:
1.wenn actlevel== level, dh. wenn die gesuchte Höhe der aktuellen Höhe entspricht, so wird 1 zurückgegeben und die Rekursiv bricht ab, sodass seine eventuell weiteren Kinder nicht mehr betrachtet werden.
Wobei es ja sogar egal ist, ob die betrachtet werden, weil dann immer actlevel > level ist.
fy06keju hat geschrieben: 2. falls die aktuelle Höhe nicht der gesuchten Höhe entspricht, so ruft sich der Algorithmus rekursiv auf. Der rekursive Aufruf erfolgt für den linken sowie den rechten Nachfolger des aktuellen Knotens.Nach der Induktionsvoraussetzung gilt, dass die beiden rekursiven Aufrufe für den linken und rechten Teilbaum der 'wurzel' korrekt sind. Dabei wird korrekterweise die aktuelle Höhe 'level' um eins inkrementiert. Schließlich werden die Ergebnisse der beiden rekursiven Aufrufe zusammen addiert, sodass am Ende korrekterweise die Gesamtanzahl der Knoten auf der gesuchten Höhe zurückgegeben wird.
Ok.
fy06keju hat geschrieben: Korrektheit: Aufgrund der Variante und Abbruchbedingung folgt, dass der Algorithmus nach endlich vielen Rekursionsschritten terminiert und die Invariante garantiert die Korrektheit des Ergebnisses.
Ok.

KW

fy06keju
Neuling
Neuling
Beiträge: 7
Registriert: 5. Sep 2016 16:52

Re: Korrektheitsbeweis rekursiv Binärbaum

Beitrag von fy06keju » 17. Sep 2016 10:06

Vielen Dank !!

Antworten

Zurück zu „AuD: Theoretische Aufgaben“