Angewandte Softwareverifikation mit einem interaktiven Theorembeweiser Version 28. März 2011

Balancierte binäre Bäume

Mit balancierten binären Suchbäumen vermeidet man, dass ein Baum zu einer Liste degeneriert. Perfekt ausbalancierte Bäume sind dabei meist nicht erstrebenswert. Es reicht aus, wenn die Bäume nicht zu unbalanciert sind.

Aufgabe

1. Definieren Sie nahezu balancierte binäre Bäume als predikativen Teiltyp eines geeigneten Typs für binäre Bäume.

2. Definieren Sie Funktionen zum Einfügen, Löschen und Suchen in nahezu balancierten binären Suchbäumen.

3. Beweisen Sie, dass diese Funktionen die entsprechenden Invarianten erhalten (der Baum bleibt ein nahezu balancierter binärer Suchbaum).