ich habe mir nochmal Mühe bei einem rekursiven Induktionsbeweis gegeben und probiert die Dinge gemäß Vorlagen und Beispiele auf den Punkt zu bringen. Der Code prüft die Verzeigerungsstruktur eines Multi-Way-Trees.
Code: Alles auswählen
public boolean isTreeCorrect(TreeNode<T> r) {
if (r == null)
return true;
HashSet<TreeNode<T>> set = new HashSet<TreeNode<T>>();
return isTreeCorrectRec(r, set);
}
public boolean isTreeCorrectRec(TreeNode<T> m, HashSet<TreeNode<T>> set) {
if (!set.add(m))
return false;
if (m.theSuccessors != null)
for (int i = 0; i <= theSuccessors.length; i++)
if (!isTreeCorrectRec(theSuccessors[i], set))
return false;
return true:
}
Induktionsbeweis:
Input:
- m != null
- Eine korrekte HashSet
Output:
- True, falls die Verzeigerungsstruktur des Vielwegbaums korrekt gebildet ist
- False, falls dem nicht so ist.
Invariante:
Unmittelbar nach einem rekursiven Schritt liefert der Algorithmus true, wenn m ein korrekt verzeigerter Knoten in einem Vielwegbaum ist. Andernfalls liefert der Algorithmus false und bricht die komplette Rekursion ab.
Induktionsparameter:
- Höhe eines Teilbaums
Induktionsanfang:
Besteht der Vielwegbaum lediglich aus der Wurzel, dann ist m.theSuccessors == NULL, so bricht die Rekursion ab und der Algorithmus liefert true.
Induktionsvoraussetzung:
Sei n > 0 die höhe eines Teilbaums. Für die Höhe m (wobei 0 <= m < n gilt) eines Teilbaums ist dieser Teilbaum ein korrekt verzeigerter Vielwegbaum.
Induktionsschritt:
Nach der Induktionsvoraussetzung gilt für einen Teilbaum \(T'\) von \(T\), dass \(T'\) korrekt gebildet ist. In diesem rekursiven Schritt wird nun, ein Knoten \(v \in U, U := T \backslash T'\) betrachtet. Ist \(v\) bereits in der HashSet enthalten (also der Menge der bereits gesichteten Knoten), bricht die komplette Rekursion ab und der Algorithmus liefert false, da \(U \bigcap T' = \emptyset\) gilt für eine korrekte Verzeigerungsstruktur. Andernfalls wird \(v\) der HashSet hinzugefügt und der Algorithmus überprüft für die Nachfolger von \(v\) ob diese richtig gebildet wurden.
Wohldefiniertheit:
- Keine ArithmeticException, da keine Arithmetischen Operationen durchgeführt werden
- Keine NullpointerException, da m != NULL
- Kein Überlauf oder NaN
Terminierung:
Der Algorithmus terminiert, da der Baum endliche Tiefe besitzt und nach jedem rekursiven Aufruf eine ebene Tiefer in den Baum gegangen wird. Besitzt der Baum eine falsche Verzeigerungsstruktur, so terminiert der Algorithmus vorzeitig.
Korrektheit:
Aus Invariante und Abbruchbedingung folgt die Korrektheit des Algorithmus. (Hier weiß ich nicht was ich noch schreiben könnte. Im Muster steht, dass man bei Rekursionen die in eigene Methoden ausgelagert werden Zusatzargumente benötigt werden
Komplexität:
Best Case:
Im Best Case ist m.theSuccessors == NULL und wir erhalten somit \(O(1)\).
Worst Case
Es handelt sich um einen korrekt gebildeten Vielwegbaum. Somit muss jeder Knoten betrachtet werden und wir erhalten \(O(n)\).
Danke für den Hinweis
)