Verbesserung von Zertifizierern für Terminierungsbeweise

Terminierung (jede Berechnung kommt zu einem Ende) ist eine fundamentale Eigenschaft von Programmen. Obwohl diese Eigenschaft im Allgemeinen unentscheidbar ist, gibt es zahlreiche Arbeiten zum Thema automatische Terminierungsanalyse. In diesem Antrag konzentrieren wir uns auf die Terminierungsanalyse von Termersetzungssystemen, einem einfachen, aber dennoch mächtigen Berechenbarkeitsmodell, welches zu großen Teilen der deklarativen Programmierung, sowie dem automatischen Beweisen zu Grunde liegt. Die Motivation ist, dass die Terminierungsanalyse von Programmen in den verschiedensten Programmiersprachen, oft mit Hilfe der Termersetzung durchgeführt werden kann. Es gibt zum Beispiel Transformationen von Prolog, Haskell und Java in Termersetzungssysteme, so dass die Terminierung des resultierenden Ersetzungssystems die Terminierung des ursprünglichen Programms beweist. In der jüngsten Vergangenheit gab es einiges an Fortschritt bei der Ermittlung von hinreichenden und automatisierbaren Kriterien für die Terminierung von Termersetzungssystemen, die auch implementiert wurden. Die entsprechenden Programme (Terminierungstools) nutzen oft das Dependency Pair Framework und sind dadurch in der Lage, verschiedenste Terminierungskriterien modular zu kombinieren. Terminierungsbeweise werden hierbei durch eine Baumstruktur dargestellt, bei der jeder einzelne Knoten für die Anwendung einer bestimmten Terminierungstechnik steht. Dabei ist es keine Seltenheit, dass moderne Terminierungstools (im vollautomatischen Modus) Beweise finden, die einige Megabyte groß sind. Es geschieht jedoch immer wieder, dass ein Terminierungstool einen falschen Beweis erzeugt - es wurden auch Terminierungsbeise für nicht-terminierende Systeme generiert. Daher wird es als äußerst wichtig angesehen, die Korrektheit solcher generierten Beweise unabhängig zu zertifizieren. Durch die schiere Größe mancher Beweise kommt eine Inspektion von Hand nicht in Frage, und wäre zudem fehleranfällig. Allerdings sind interaktive Theorembeweiser, wie Coq, Isabelle oder PVS, in der Lage, diese Herausforderung zu bewältigen. Solche Theorembeweiser werden verwendet, um eine Vielzahl von Fakten aus der Mathematik, über Programmiersprachen und vieles mehr, innerhalb eines logischen Systems zu modellieren und anschließend zu verifizieren, dass bestimmte Eigenschaften erfüllt sind. Das Zertifizieren von Terminierungsbeweisen wird üblicherweise in zwei Stufen durchgeführt: Zuerst wird mittels eines Theorembeweisers formal die Korrektheit von Terminierungstechniken bewiesen. Danach wird zertifiziert, dass jeder Knoten eines gegebenen Beweisbaumes einer gültigen Anwendung einer dieser Terminierungstechniken entspricht. Beispielsweise wird in der ersten Stufe ein für allemal bewiesen, dass es sich bei der lexikographischen Pfadordnung um eine Reduktionsordnung handelt. In der zweiten Stufe wird dann für eine gegebene Präzedenz und ein gegebenes Ersetzungssystem überprüft, ob alle Regeln durch die resultierende lexikographische Pfadordnung orientiert werden können. Dadurch kann man sowohl auf fehlerhafte Theoreme als auch auf Fehler von Terminierungstools stoßen. Im Moment gibt es drei unabhängige Zertifizierer. Unser Zertifizierer, IsaFoR/CeTA (zu finden auf http://cl-informatik.uibk.ac.at/software/ceta/), wurde unter Verwendung von Isabelle/HOL entwickelt. Alle drei Zertifizierer verwenden die oben beschriebene, zweistufige Herangehensweise, um Terminierungsbeweise zu zertifizieren. Als Eingabe erwarten sie einen Terminierungsbeweis in einem gemeinsamen Beweisformat, um anschließend zu entscheiden, ob dieser Beweis gültig ist oder nicht. Mit Hilfe dieser Zertifizierer wurden sowohl Fehler in Theoremen aus Publikationen als auch Fehler in Terminierungstools gefunden und konnten behoben werden. Das Ziel dieses Projekts ist es, die Anwendbarkeit unseres Zertifizierers IsaFoR/CeTA zu erhöhen. Dabei wollen wir uns mit den folgenden vier Punkten beschäftigen: A) Mehr Terminierungstechniken unterstützen, um die Anzahl der zertifizierbaren Beweise zu erhöhen. B) CeTA direkt mit Terminierungstools verbinden, so dass große Teile eines Beweises auch dann zertifiziert werden können, wenn nicht alle benutzten Techniken formalisiert wurden. C) Terminierung von Isabelle/HOL Funktionen beweisen, indem Beweise von Terminierungstools mit Hilfe von IsaFoR nach Isabelle/HOL importiert werden. Dies wird den Automatisierungsgrad des interaktiven Beweisers Isabelle/HOL erhöhen. D) Das Zertifizieren impliziter Komplexitätsschranken von Terminierungsbeweisen, um nicht nur sichere Aussagen über die Terminierung eines Systems, sondern auch über dessen Laufzeit machen zu können.

Für Computer Programme in sicherheitskritischen Bereichen (wie z.B. Luftfahrt, Brandmeldung, und medizinische Geräte) ist es sehr wichtig, dass sie zuverlässig arbeiten. Deshalb haben wir in diesem Projekt zwei wesentliche Eigenschaften von Programmen betrachtet: ein Programm terminiert, wenn es immer ein Resultat liefert und nicht endlos rechnet; und die Komplexität beschreibt, wie lange man auf das Resultat warten muss. Für beide Eigenschaften gibt es Analyse-Tools, die für viele Programme automatisch die Komplexität und das Terminierungs-Verhalten bestimmen.Es besteht jedoch das Risiko, dass die Analyse-Tools selber Fehler enthalten und falsche Antworten geben, z.B. eine Terminierung-Behauptung für ein nicht terminierendes Programm. Um dieses Risiko abzuschwächen, kann man verlangen, dass die Analyse-Tools auch ein Zertifikat erzeugen, das eine Argumentation beinhaltet, warum die gegebene Antwort richtig ist. Diese Zertifikate können dann automatisch mit Hilfe eines Zertifizierers überprüft werden. Hierbei muss die Fehlerfreiheit des Zertifizierers durch einen aufwändigen formalen Beweis nachgewiesen werden. Die Zertifizierung ist üblicherweise nur dann anwendbar, wenn alle angewandten Analyse-Techniken im Zertifikat auch vom Zertifizierer unterstützt werden, was oft die Anwendbarkeit einschränkt. Um diese zu erhöhen, haben wir in diesem Projekt die Korrektheit vieler Analyse-Techniken formal im Beweis-Assistenten Isabelle nachgewiesen und in unseren Zertifizierer integriert.Da viele Terminierungs-Techniken nur auf konfluente Programme anwendbar sind (in denen alle Berechnungen zum selben Ergebnis führen), haben wir als Nebenprodukt auch die Unterstützung für Konfluenz-Analyse-Tools in den Zertifizierer integriert. Des Weiteren unterstützt er nun auch partielle Zertifikate. In diesem Fall sieht eine typische Antwort des Zertifizierers so aus, dass 90 % der Argumentation überprüft werden konnte. Durch die Erweiterung des Zertifizierers konnten mehrere Fehler in aktuellen Analyse-Tools gefunden werden, die seit vielen Jahren unentdeckt blieben. Dies beinhaltet Implementierungsfehler, und Fehler in publizierten Fachartikeln, die leider meist nur informelle Korrektheit-Beweise beinhalten.