Automatisierung der Infrastruktur für Termersetzung

Die Erstellung von zuverlässiger Software ist eine herausfordernde Aufgabe. Kleine Fehler in Programmen können dazu führen, dass Berechnungen nicht beendet werden oder widersprüchliche Resultate liefern. Verallgemeinert spricht man hier von (Nicht-)Terminierung und (Nicht-)Konfluenz. Forschungsgruppen in der ganzen Welt entwickeln deshalb Tools zur vollautomatischen Analyse von Terminierung und Konfluenz. Diese Tools treten in jährlichen Wettbewerben gegeneinander um, wobei die Wettbewerbe selber von der Forschungsgemeinschaft organisiert werden. Dieses Österreich-Japan Projekt widmet sich der Entwicklung einer Infrastruktur, um Forscher im Bereich der Terminierungs- und Konfluenz-Analyse zu unterstützen, d.h. sowohl Tool-Autoren als auch Organisatoren von Wettbewerben. Dabei liegt der Fokus auf Termersetzungssystemen, einer einfachen Programmiersprache, die in diesem Bereich häufig verwendet wird. Das Projekt hat drei Hauptziele. Zuerst werden wir eine Software Infrastruktur entwickeln, um Analyse Tools in den genannten Bereichen zu evaluieren. Diese wird die Durchführung von Wettbewerben, wie z.B. der "Confluence Competition" (CoCo) und der "Termination and Complexity Competition" (termCOMP), stark erleichtern. Die Infrastruktur ermöglicht ebenfalls einen unkomplizierten Zugriff auf die teilnehmenden Analyse Tools und auf die Eingaben, die diese bekommen. Weil die Eigenschaften wie Terminierung und Konfluenz unentscheidbar sind, und weil die Analyse Tools selber komplexe Programme sind, können auch hier Fehler passieren, so dass bei den Wettbewerben widersprüchliche Analysen generiert werden. Aufgrund der Komplexität der Analysen kann eine manuelle Inspektion oft nicht sicherstellen, ob eine Analyse fehlerfrei ist. Deswegen werden Prüfprogramme zur Validierung eingesetzt, deren eigene Korrektheit in Beweis-Assistenten formal verifiziert wurde. Da solche formalen Beweise jedoch sehr aufwändig sind, unterstützen die Prüfprogramme nicht alle Arten von Analysen, insbesondere werden Prüfungen für mehrere der neueren Wettbewerbe innerhalb der CoCo kaum unterstützt. Der Ausbau der Prüfungen in diesem Bereich ist deshalb das zweite Ziel dieses Projekts. Das dritte Ziel ist die Entwicklung neuer Analyse Techniken für eine Erweiterung von Termersetzungssysteme, welche darin besteht, dass zusätzlich logische Bedingungen formuliert werden dürfen, was z.B. im Bereich der Programm-Verifikation oft nützlich ist. Neben Konfluenz Analyse für diese erweiterten Systeme sollen auch Techniken aus dem Bereich Induktives Beweisen untersucht werden. Die erwarteten Resultate des Projekts sind eine Software Infrastruktur, die von CoCo und termCOMP genutzt wird und auch für andere Wettbewerbe nützlich sein könnte. Die ausgebauten verifizierten Prüfprogramme werden zu erhöhter Zuverlässigkeit der Analyse Tools führen. Und die erweiterten Termersetzungssysteme führen zu einer besseren Anwendbarkeit in der Programm-Verifikation.

Automatisierung der Infrastruktur für Termersetzung (ARI) Es ist eine herausfordernde Aufgabe, zuverlässige Software zu erstellen. Fehler im Quellcode können zu Programmen führen, die nicht-endende Berechnungen durchführen, oder die unterschiedliche Ausgaben liefern, obwohl eindeutige Resultate erwünscht wären. Im Abstrakten sind diese Eigenschaften als (Nicht-)Terminierung und (Nicht-)Konfluenz bekannt. Weltweit gibt es Forschungsteams, die Tools entwickeln, um vollautomatisch Eigenschaften wie Konfluenz und Terminierung von gegebener Software zu beweisen oder zu widerlegen. Um ihre Analysestärke zu demonstrieren, treten diese Tools in jährlichen Wettbewerben gegeneinander an, die von der Forschungsgemeinschaft organisiert werden. Im Rahmen dieses Gemeinschafts-Projekt zwischen Österreich und Japan wurde eine Infrastruktur entwickelt, um Forscher im Bereich der Konfluenz- und Terminierungs-Analyse zu unterstützen. Die Infrastruktur dient sowohl Autoren von Tools als auch Organisatoren von Wettbewerben. In dem erwähnten Forschungsbereich werden Programme oft als Termersetzungssysteme repräsentiert, eine einfache aber Ausdrucks-starke Abstraktion. Die neue ARI Infrastruktur, die in diesem Projekt entwickelt wurde, beinhaltet ARI-COPS, eine Datenbank für Konfluenz Probleme und für Resultate aus Wettbewerben, sowie ARIWeb, ein leicht zugängliches Web-Interface für Tools, die beim jährlich Konfluenz-Wettbewerb teilnehmen. Sowohl ARI-COPS als auch ARIWeb basieren auf dem neuen ARI Format für Termersetzungssysteme, auf einem Konvertierungs-Tool für verschiedene Formate, auf Zertifizierern von Resultaten aus Wettbewerben, und auf einen Tool zur Entdeckung von Duplikaten. Die ARI Infrastruktur ist verfügbar unter: https://ari-cops.uibk.ac.at/ Weil die Eigenschaften in den Konfluenz- und Terminierungs-Wettbewerben im Allgemeinen unentscheidbar sind, und weil die teilnehmenden Tools oft sehr komplexe Programme sind, können fehlerhafte Analysen in den Tools nicht ausgeschlossen werden, und es kann zu widersprüchlichen Analysen während der Wettbewerbe kommen. In solchen Situationen ist es oft nicht möglich, die richtige Analyse durch manuelle Inspektion zu bestimmen. Deshalb wurden Zertifizierer entwickelt, die Analysen automatisch validieren können, und deren Korrektheit in Beweis-Assistenten formal nachgewiesen wurde. Im Rahmen dieses Projekts wurden diese Zertifizierer weiter ausgebaut, und wir erwähnen hier zwei Beispiele. (1) Es wurde eine Konfluenz-Technik unterstützt, die auf simultanen kritischen Paaren und Beweistermen basieren, um Berechnungen zu repräsentieren. Diese Technik wurde erstmals nach über 10 Jahren formalisiert. (2) Ein neuer Algorithmus wurde entwickelt, um nachzuweisen, ob die linken Seiten eines funktionalen Programms alle Fälle bzgl. Pattern Matching abdecken. Der neue Algorithmus hat eine formal nachgewiesene optimale asymptotische Komplexität. Des weiteren wurden neue Techniken zur Analyse von solchen Termersetzungssystemen entwickelt, die auch logische Bedingungen zur Berechnung erlauben, die dann mit leistungsstarken SMT-Solvern geprüft werden. Diese sogenannten "logically constrained term rewrite systems" (LCTRS) finden immer weitere Verbreitung in der Programmverifikation. Eine maßgeschneiderte Transformation von LCTRSen zu normalen Termersetzungssysteme erlaubte es, viele bekannte Konfluenz-Techniken von Termersetzungssysteme auf LCTRS zu verallgemeinern. Diese Techniken für LCTRS wurden im Tool "crest" implementiert, welches die LCTRS Kategorie beim Konfluenz-Wettbewerb dominiert.