Korrektheitsbeweis rekursiv Binärbaum

[fy06keju]

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]

Hier mein Code:

Sieht für mich auf den ersten Blick gut aus.

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.

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.

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.

Variante: die Höhe des Baumes, auf die die wurzel zeigt, nimmt ab

Ok.

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

Ja, reicht, da offensichtlich korrekt.

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.)

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

Ok.

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.

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.

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]

Vielen Dank !!