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

Rot-schwarze Bäume

Rot-schwarze Bäume sind eine einfachere Form balancierter binärer Bäume. In rotschwarzen Bäumen haben die Knoten ein, zwei oder drei Nachfolgeknoten. Dadurch kann man einen beliebigen Knoten immer leicht erweitern. Implementiert werden rotschwarze Bäume mit binären Bäumen, in denen die Knoten gefärbt sind (nämlich rot oder schwarz). Jeweils zwei oder drei solche gefärbter Knoten entsprechen dann einem Knoten im abstrakten rot-schwarzen Baum.

Aufgabe

1. Definieren Sie rot-schwarze 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 rot-schwarzen Suchbäumen.

3. Beweisen Sie, dass diese Funktionen die entsprechenden Invarianten erhalten (der Baum bleibt ein rot-schwarzer Suchbaum).

4. Es ist ausreichend rot-schwarze Bäume über natürlichen Zahlen zu betrachten.