Automatische Amort. Ressourcenanalyse von Datenstrukturen

Algorithmen spielen eine zentrale Rolle in der Wissenschaft und der Praxis der Datenverarbeitung. Oft sind wir jedoch nicht nur daran interessiert "welche" Aufgabe ein bestimmter Algorithmus ausführt, z. B. das Sortieren eines Kartenspiels, sondern auch, "wie effizient" diese Aufgabe ausgeführt wird. Das heißt, über die Korrektheit eines Algorithmus hinaus ("ob er die Aufgabe wie beabsichtigt ausführt oder nicht"), sind wir an seiner Effizienz interessiert und wollen seine Komplexität ("die Ausführungszeit") analysieren. Ein Maß für die Komplexität eines Algorithmus oder einer Datenstruktur ist seine amortisierte Komplexität. Stellen Sie sich vor, Sie haben eine Sammlung von Objekten, z.B. ein Kartenspiel, und Sie möchten wissen, wie lange es dauert, eine Aufgabe für alle Objekte durchzuführen. Wenn Sie die maximalen Kosten der Aufgabe für ein einzelnes Objekt betrachten und diese Kosten mit der Anzahl der Objekte multiplizieren, erhalten Sie eine Obergrenze für die gesamten Kosten. Aller Wahrscheinlichkeit nach wäre die so erhaltene Obergrenze jedoch zu grob, da die Erledigung der Aufgabe für bestimmte Objekte langsamer oder schneller sein kann. An dieser Stelle kommt eine amortisierte Analyse ins Spiel. Für einen bestimmte Aufgabe können bestimmte Situationen erhebliche Ressourcenkosten verursachen, während andere Situationen weniger kostspielig sind. Bei der Amortisationsanalyse werden sowohl die kostspieligen als auch die weniger kostspieligen Vorgänge über die gesamte Vorgangsabfolge hinweg berücksichtigt. Zusammenfassend lässt sich sagen, dass die amortisierte Analyse eine Methode zur Kostenanalyse ist, bei der einzelne Operationen als Teil einer Abfolge von Operationen betrachtet wird. Die Kostenanalyse anspruchsvoller Datenstrukturen, wie z.B. selbstanpassender binärer Suchbäume, war bereits im ursprünglichen Entwurf der amortisierten Analyse ein Hauptziel. Die Analyse dieser Datenstrukturen erfordert eine aufwendige manuelle Komplexitätsanalyse (mit Bleistift und Papier). In früheren Arbeiten haben wir erste Schritte in Richtung einer vollautomatischen amortisierten Analyse unternommen. Abgesehen von unserem Pilotprojekt gabe es eine solche Analyse bislang nicht. In diesem Projekt zielen wir auf eine automatisierte Analyse der gebräuchlichsten Datenstrukturen mit guter, d.h. sublinearer, Komplexität ab, wie sie typischerweise in Standardbibliotheken verwendet werden. Unsere Ziele sind die Verifikation von Datenstrukturen in Lehrbüchern, die Bestätigung und Verbesserung von zuvor gefundenen Komplexitätsschranken sowie die automatisierte Analyse von realistischen Implementierungen. Anfangs werden wir uns auf streng funktionale Programmiersprachen (erster Ordnung) beschränken. Später werden wir unsere Forschung in Richtung lazy evaluation ausweiten, um die Analyse von persistenten Datenstrukturen zu ermöglichen. Außerdem werden wir auch probabilistische Datenstrukturen berücksichtigen.