Ich habe mir für diese rekursive Methode einen Korrektheitsbeweis aufgeschrieben.
Code: Alles auswählen
boolean hasPathSum(Node node, int sum) {
// return true if we run out of tree and sum==0
if (node == null) {
return(sum == 0);
}
else {
// otherwise check both subtrees
int subSum = sum - node.key;
return(hasPathSum(node.left, subSum) || hasPathSum(node.right, subSum));
}
}
Die Wurzel eines korrenten BinaryTrees, Wurzel kann auch =null sein.
Sum ist in Integer >= 0.
Output:
True gdw. ein Pfad von der Wurzel bis zu einem Blatt im Baum gibt, dessen Keys
zusammenaddiert gleich der gegebenen summe (sum) ist.
False gdw. es keinen Pfad im Baum gibt deren Summe aufaddiert gleich sum ist.
Wohldiefiniertheit:
Keine NullPointerException, da es im Code geprüft wird.
Keine ArithmeticException, da es keine Instruktionen gibt die einen Überlauf verursachen.
Differenz von Sum und addierten Keys >= INTEGER.MIN_VALUE sein
Terminierung:
node==null
Variante:
Nach jeden Rekursionsschritt steigt man eine Stufe tiefer im Baum.
Invariante:
Unmittelbar nach einem Rekursionsschritt gilt, das subSum das Ergebnis von sum - aller bis j
jetzt besuchten Knoten im aktuellen Pfad.
Induktionsparameter:
Höhe des Baumes m und subSum.
Ind Anfang:
Ist der Baum gleich null, so bricht der Algorithmus ab und liefert True falls die Summe = 0 ist.
Induktionsschritt:
Für die Höhe m-1 hat man m-1 Knoten im aktuellen Pfad besucht und subSum enthält bis jetzt das Ergebnis von
sum - m-1 Knoten-Keys.
Da wir jetzt einen Stufe tiefer im Baum abgestiegen sind, also für die Höhe m,
enthält subSum das Ergebnis von sum - m-1 Knoten Keys -1 den Wert des m-ten Keys.
Korrektheit:
Dank der Variante und der Abbruchbedingung terminiert der Algorithmus nach endlich viele Schritte und liefert das Korrekte
Ergebnis, gemäß der Invariante.
Viele Grüße.