Zertifizierte Terminierung und Komplexität von Programmen

Terminierung (alle Berechnungen führen zu einem Ergebnis) und Komplexität (wie lange dauert die Berechnung, und wie hoch ist der Speicherbedarf) sind fundamentale Eigenschaften eines Programms. Obwohl diese Eigenschaften im Allgemeinen unentscheidbar sind, wurden viele Verfahren für deren automatische Analyse entwickelt. Obwohl die Antwort entsprechender Tools sehr einfach ausfallen kann (ja, dieses Programm terminiert), ist der zugrundeliegende Beweis meist nicht einfach. Es ist ein Fakt, dass viele Tools für die automatische Analyse der Komplexität und Terminierung selbst komplex sind, und intern verschiedenste Verfahren kombinieren, um das Verhalten eines Programms zu analysieren. Folglich können diese Tools Fehler enthalten, die zu falschen Antworten und Beweisen führen. Eine Lösung zu diesem Problem bieten Zertifizierer, welche die generierten Beweise der Tools validieren können. Um die Korrektheit der Zertifizierer zu gewährleisten, wird diese in einem Theorem-Beweiser formal nachgewiesen. Mit Hilfe solcher Zertifizierer konnten bereits viele Fehler entdeckt werden, sowohl in den Implementierungen der Tools als auch in den Korrektheitsbeweisen der Terminierungstechniken. Leider ist die Anwendbarkeit der verfügbaren Zertifizierer in diesem Gebiet recht eingeschränkt: die unterstützten Techniken sind meist für Terminierung-Beweise und nicht für Komplexitäts-Beweise; zudem sind die Zertifizierer eingeschränkt auf Termersetzung, einem einfachen, aber dennoch mächtigen Berechenbarkeitsmodell, welches zu großen Teilen der deklarativen Programmierung, sowie dem automatischen Beweisen zu Grunde liegt. In diesem Projekt werden wir die Anwendbarkeit der Zertifizierer in zwei wichtige Richtungen erweitern: sie sollen eine große Klasse von Komplexitäts-Beweisen unterstützen, sowie Terminierungs-Beweise für zwei reale Programmiersprachen, Java und Haskell. Zu diesem Zweck werden wir viele interessante Formalisierungen entwickeln, wie etwa eine umfassende Bibliothek über lineare Algebra, die für die Zertifizierung von Komplexitäts-Beweisen notwendig ist. Des Weiteren werden wir die Arbeit von Klein und Nipkow über Jinja in Richtung Java ausbauen, und wir werden eine Semantik für Haskell formalisieren. Unsere Arbeit wird die Zuverlässigkeit aktueller Termierungs- und Komplexitäts-Tools weitreichend verbessern. Ferner bietet sie einen guten Ausgangspunkt für weitere Formalisierungen in dem Gebiet der Programm-Analyse und der Programm-Transformation.

Computer-Programme dringen in immer mehr Bereiche unseres Lebens ein: sie verwalten unser Geld, steuern Abläufe in Fahrzeugen und kontrollieren medizinische Geräte. Deshalb ist es wichtig, dass Programme richtig funktionieren. Hierbei sind Terminierung (alle Berechnungen führen zu einem Ergebnis) und Komplexität (wie lange dauert die Berechnung, und wie hoch ist der Speicherbedarf) fundamentale Eigenschaften eines Programms. Leider sind diese fundamentalen Eigenschaften unentscheidbar: es ist z.B. nicht möglich, ein Analyse-Programm zu entwickeln, das für alle anderen Programme angibt, ob sie terminieren oder nicht. Trotzdem wurden viele Verfahren für die automatische Analyse entwickelt, die oft, aber nicht immer die gewünschte Eigenschaft nachweisen können. Obwohl die Antwort entsprechender Analyse-Programme sehr einfach ausfallen kann (ja, dieses analysierte Programm terminiert), ist die Argumentation, warum die erzeugte Antwort richtig ist, also der zugrundeliegende Beweis, meist nicht einfach. Es ist ein Fakt, dass viele Analyse-Programme für Komplexität und Terminierung selbst komplex sind, und intern verschiedenste Verfahren kombinieren, um das Verhalten eines Programms zu analysieren. Folglich können die Analyse-Programme Fehler enthalten, die zu falschen Antworten und falschen Beweisen führen. Unsere Lösung des Problems besteht aus dem Programm CeTA (Certified Tool Assertions), ein Zertifizierer, der in diesem Projekt entwickelt wurde. CeTA kann überprüfen, ob ein generierter Beweis eines Analyse-Programms korrekt ist oder nicht. Um die Korrektheit von CeTA selber sicherzustellen, wurden alle Algorithmen, die CeTA intern verwendet, formal mittels des Theorem Beweisers Isabelle verifiziert. Im Vergleich zu vorigen Zertifizierern hat CeTA folgende Alleinstellungsmerkmale: - CeTA unterstützt viele Arten von Komplexitätsbeweisen von verschiedenen Analyse-Programmen. - CeTA unterstützt die Prüfung von Terminierungsbeweisen von LLVM, einer weit-verbreiteten Zwischensprache, die zur Übersetzung populärer Programmiersprachen wie C und Haskell genutzt wird. - Um Komplexitätsbeweise zu prüfen, nutzt CeTA intern präzise Berechnungen mit algebraischen Zahlen. Zum Beispiel kann CeTA alle Nullstellen eines Polynoms wie x^8 - 5x^6 + 7x^3 - 17 ohne Rundungsfehler bestimmen. - Um Terminierungsbeweise für LLVM zu prüfen, bietet CeTA eine Methode zur Lösung von linearen Ungleichungen an. Zum Beispiel kann CeTA herausfinden, ob es ganze Zahlen x, y und z gibt, welche die Ungleichungen 2x + 3y - 2z > 7, x - 5y + 4z > -2 und 3x + 4y + z < 15 erfüllen. Weitere Ergebnisse dieses Projekts sind aufgedeckte (und korrigierte) Fehler in Fachbüchern und Fachartikeln, die während der Formalisierung gefunden wurden. Zudem hat CeTA mehrere Fehler in generierten Beweisen entdeckt, so dass Fehler in den entsprechenden Analyse-Programmen korrigiert werden konnten. Schlußendlich bieten die verifizierten Algorithmen einen guten Startpunkt, um weitere Formalisierungen im Bereich der Programm-Analyse durchzuführen.