Korrektheitsbeweis: BinaryTree

[Hallo]

Hallo,

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)); 
  } 
}

Input:
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.

[sqrt(2)]

Hallo Hallo,

hier mal meine Variante zum Induktionsbeweis. Der kann sehr ähnlich zu deinem sein, habe ihn mir bewusst noch nicht angeschaut.

Input:
- Wurzel (node) auf einen korrekt gebildeten binären Baum (setze das mal voraus)
- Wurzel (node) kann auch null sein
- Integer Zahl sum die im Intervall der Integerzahlen liegt

Output:
- True, wenn die Summe der Keys von einem Baumpfad von Wurzel bis zum Blatt sum entspricht
- False, sonst

Wohldefiniertheit:
- ArithmeticException kann nicht vorkommen das keine unzulässige arithmetische Operation durchgeführt wird
- Overflow, kann passieren wenn subSum einen Wert annimmt der nicht im Intervall der Integerzahlen ist. Dies wird im Code nicht abgefangen.
- NullpointerException, kommt nicht vor, da der Rekursionsanker korrekt gebildet ist

Terminierung:
Der Algorithmus terminiert, sobald node == null

Variante:
In jedem rekursiven Aufruf verringert sich die Höhe des Teilbaumes

Invariante (= Induktionshypothese):
Unmittelbar nach einem rekursiven Aufruf enthält subSum die Differenz aus sum und der ausgehend von der Wurzel bisher betrachteten Knoten eines Baumpfades.

Induktionsanfang:
Im Falle das node = NULL besteht die Möglichkeit wegen (sum == 0), dass
a. sum == 0 ist und der Algorithmus terminiert mit dem korrekten Ergebnis true
b. sum != 0 ist und der Algorithmus terminiert mit dem korrekten Ergebnis false


Induktionsvoraussetzung:
Für einen echten Teilbaum T' von T liefert der Algorithmus ein korrektes Ergebnis.

Induktionsschritt:
Nach Induktionsvoraussetzung gilt, dass der Algorithmus für den betrachteten Teilbaum T' ein korrektes Ergebnis liefert. (a) Existiert ein Pfad von der Wurzel zum Blatt dessen Summe gerade sum entspricht so terminiert der Algorithmus mit dem Output true und beide Teilbäume werden nicht behandelt. (b) Existiert solch ein Pfad im linken Teilbaum, so wird dieser mit true ausgewertet, der Algo terminiert und der rechte Teilbaum wird nicht behandelt. (c) Existiert solch ein Pfad im rechten Teilbaum, wird der linke Teilbaum mit false ausgewertet und der Algorithmus terminiert mit true, da im rechten Teilbaum solch ein Pfad vorzufinden ist. Tritt keiner dieser Fälle ein termniert der Algo mit false.

Korrektheit:
Wohldefiniertheit und Terminierung waren oben schon geklärt, korrektes Ergebnis der ausgelagerten rekursiven Methode folgt ohne weitere Argumente aus der Invariante.

Komplexitätsklasse:
Best Case, node == NULL => \(\Theta(1)\) EDIT EDIT EDIT: NEIEN!! sondern wenn die Knoten vom Pfad von Wurzel zum "linkesten" Blatt die Summe \(sum\)hat. Das wäre also die Höhe des Baumes, wenn es ein balancierter Binärer Baum ist => \(\Theta(log(n))\). Ist es kein balancierter Baum, \(\Theta(n)\)
Worst Case, Kein Pfad von Wurzel zu Blatt ist in Summe = sum => \(\Theta(n)\)

[Hallo]

Push

[Hallo]

Push

[Prof. Karsten Weihe]

Oh je, trotz 2x push landen Sie immer weit hinten in der Liste ...

Code: Alles auswählen

boolean hasPathSum(Node node, int sum) { 
  // return true if we run out of tree and sum==0 
}

Ich muss gestehen, ich verstehe nicht, was Ihre Methode genau leisten soll. Das ist keine von meinen Java-Übungsaufgaben, oder?

Input:
Die Wurzel eines korrenten BinaryTrees, Wurzel kann auch =null sein.
Sum ist in Integer >= 0.

Inhaltlich ok.

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.

Ok, hier verstehe ich, was Ihre Methode machen soll. Aber das, was sie tun soll, kann sie doch unmöglich tun, wenn sie überhaupt nicht auf Attribut key zugreift

KW

[Hallo]

Die Methode greift doch auf Attribut key in:

Code: Alles auswählen

else { 
  // otherwise check both subtrees 
    int subSum = sum - node.key;
    return(hasPathSum(node.left, subSum) || hasPathSum(node.right, subSum)); 
  } 

[Prof. Karsten Weihe]

Sorry, mein Fehler, ich hatte Ihr Posting völlig missverstanden, denke aber, ich habe es jetzt verstanden. Ihr Code scheint mir ok zu sein. Ich mache dann 'mal weiter, wo ich vorhin aufgehört hatte...

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

Ok.

Terminierung:
node==null

Ok.

Variante:
Nach jeden Rekursionsschritt steigt man eine Stufe tiefer im Baum.

Ok, wobei ich schon mehrfach im Forum angesprochen hatte: Es ist sauberer, die Induktionsvariable herauszuarbeiten und diese dann explizit in der Variante anzusprechen. Bei solchen rekursiven Algorithmen auf Bäumen bietet sich als Induktionsvariable die Höhe des Teilbaumes an, der am übergebenen Knoten hängt, und die Variante ist dann, dass diese Höhe echt verringert wird.

Invariante:
Unmittelbar nach einem Rekursionsschritt gilt, das subSum das Ergebnis von sum - aller bis j
jetzt besuchten Knoten im aktuellen Pfad.

Die Invariante enthält die Aussagen, die notwendig sind, um am Ende Korrektheit des Endergebnisses zu folgern. Wie soll das mit dieser Aussage gehen?

Mein Vorschlag: Rückgabe eines Rekursionsschrittes ist true genau dann, wenn es mindestens einen Pfad vom übergebenen Knoten node hinab zu einem Blatt gibt in dem Teilbaum, dessen Wurzel node ist, so dass die Schlüsselwerte entlang des Pfades in Summe gleich dem zweiten Parameter sind.

Induktionsparameter:
Höhe des Baumes m und subSum.

Ich rate davon ab, zwei Induktionsvariable zu benennen, das kann im weiteren unnötig konfus werden. Mein Vorschlag ist, die Höhe zu nehmen (siehe oben).

Ind Anfang:
Ist der Baum gleich null, so bricht der Algorithmus ab und liefert True falls die Summe = 0 ist.

Hier sind Sie ja schon von selbst meinem Vorschlag gefolgt, die Höhe als (einzige) Induktionsvariable zu nehmen => befürchtete Konfusion vermieden.

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.

Ich muss gestehen, ich verstehe nicht ganz, was Sie dem Leser sagen wollen. Ich versuche es einmal mit einem Gegenvorschlag zum Vergleich:

Nach Induktionsvoraussetzung liefert jeder der beiden rekursiven Aufrufe true zurück genau dann, wenn es einen Pfad von node.left bzw. node.right mit Schlüsselwertsumme sum - node.key gibt. Zusammen mit node.key ergibt das Schlüsselwertsumme sum ab node, und korrekterweise liefert der betrachtete rekursive Aufruf genau dann true zurück.

Das Muster bei meinen Gegenvorschlägen bzgl. Induktionsschritt scheint mir immer dasselbe zu sein: Ich arbeite explizit heraus, was die Induktionsvoraussetzung besagt, und verknüpfe das dann damit, was in der Methode nach den rekursiven Aufrufen noch passiert.

Korrektheit:
Dank der Variante und der Abbruchbedingung terminiert der Algorithmus nach endlich viele Schritte und liefert das Korrekte
Ergebnis, gemäß der Invariante.

Ok.

KW