Bedingte Ersetzung und SMT: Aufkommende Trends in Ersetzung

Termersetzung ist ein abstraktes Berechnungsmodell, welches die theoretischen Grundlagen für die Deklarative Programmierung darstellt. Viele Eigenschaften von Termersetzungssystemen sind in den letzten Dekaden intensiv erforscht worden und seit ein paar Jahren gibt es Anstrengungen, mächtige Tools zu erstellen, welche Eigenschaften von Termersetzungssystemen automatisch nachweisen. Dieses Joint Project bündelt Kräfte der Universität Innsbruck/Technischen Universität Wien mit vier Forschungsgruppen aus Japan (Hokkaido University, Japan Advanced Institute of Science and Technology, Nagoya University, University of Yamanashi) und behandelt die folgenden fünf Ziele: 1. Bedingte Ersetzung 2. SMT (Satisfiability Modulo Theories) 3. Vervollständigung 4. Komplexität 5. Zertifizierung Das Grundziel ist die Anwendbarkeit von Ersetzungstechniken in der Verifikation zu erhöhen. Dies geschieht durch den Einsatz von Bedingter Ersetzung, einem Paradigma welches für die Programmanalyse besser geeignet ist als Unbedingte Ersetzung. Bedingte Ersetzung ist ein wohlerforschtes Gebiet, allerdings gibt es verschiedene Ansätze und nur wenige Versuche zur Automatisierung dieser Techniken. Deshalb ist ein gründlicher Vergleich zwischen diesen Ansätzen eine nichttriviale Aufgabe. In diesem Projekt werden wir verschiedene Ansätze vergleichen, z.B. durch einen Wettkampf von Tools. Heutzutage verwenden viele Ersetzungstools sogenannte SMT-Löser als externe Software, welche (erweiterte) Boolesche Formeln lösen. Das zweite Ziel des Projekts ist es, (bestehende) Ersetzungstools mächtiger zu machen, indem die zugrundeliegenden SMT-Löser mit direkter Unterstützung für Bedinge Ersetzung ausgestattet werden. SMT-Löser sind auch für Varianten und Erweiterungen der (Knuth- Bendix)Vervollständigung unabdingbar, welche in Ziel 3 formuliert sind. Ziel Nummer 4 is es, obere Grenzen für die Komplexität von Programmen automatisch zu finden; auch hier sind die Errungenschaften von den Zielen 1 und 2 essentiell. Schlussendlich beschäftigt sich Ziel 5 mit der Korrektheit der vorher genannten Ansätze, d.h., die Ausgabe von einem Tool wird mittels eines Theorembeweisers automatisch überprüft.

Das Grundziel dieses gemeinsamen Forschungsprojekts zwischen zwei österreichischen Universitäten und vier Universitäten in Japan war es den aktuellen Stand in der bedingten Ersetzung, sowie der Anwendbarkeit von SMT-Lösern in der Termersetzung, voranzutreiben. Termersetzung ist ein abstraktes Berechnungsmodell, in dem Mengen gerichteter Gleichungen verwendet werden, um Ausdrücke umzuformen, zum Beispiel, um sie zu vereinfachen. Solche Systeme aus Ersetzungsregeln können beliebige Computerprogramme beschreiben. Dank ihrer einfachen theoretischen Grundlage, bildet die Untersuchung von Termersetzungssystemen ein attraktives Sprungbrett zur Entwicklung von Techniken für die Analyse von Programmen aus praktischen Anwendungen. Bedingte Ersetzung ist eine wichtige Variante der Termersetzung in der Ersetzungsregeln mit Bedingungen versehen werden, die es erlauben ihre Anwendbarkeit zu präzisieren. Dies macht sie besser geeignet für die Programmanalyse. Ein wichtiger Beitrag dieses Projekts ist die Entwicklung eines umfassenden Framework für Ersetzung mit logischen Bedingungen. Ein Software-Tool, basierend auf mächtigen SMT- Lösern, wurde entwickelt um dieses Framework zu unterstützen. Bei- de wurden erfolgreich in der Programmverifikation eingesetzt: Ein großer Teil der Programmiersprache C wurde in das Framework übersetzt, sodass Aufgabenstellungen der Verifikation automatisch beantwortet werden können. Ein weiterer wichtiger Beitrag ist die Entwicklung eines Begriffs von Komplexität für bedingte Ersetzung. Komplexität misst die Menge der benötigten Ressourcen für eine Berechnung. Unser neuer Komplexitätsbegriff ist realistisch, indem er nicht nur erfolgreiche Berechnungen misst, sondern auch Teilberechnungen, die in einer fehlgeschlagenen Regelandwendung enden. Experimente mit der auf bedingter Termersetzung basierenden Ausführungsumgebung Maude zeigen die praktische Relevanz. Mehrere Techniken zur automatischen Tool-Unterstützung, um enge obere Schranken für die Komplexität von bedingten Ersetzungssystemen zu bestimmen, wurden vorgeschlagen. Der letzte Beitrag den wir hier erwähnen, sind Untersuchungen zu AC-KBO, einer Terminierungsmethode fürErsetzungssysteme mit Assoziativitäts- und Kommutativitätsaxiomen. Experimentelle Ergebnisse zur Terminierungsanalyse und zur Vervollständigung (bei der das Ziel darin besteht ein gegebenes System von Axiomen in eine auf einem Ersetzungssystem basierte Darstellung zu überführen) zeigen klar die Vorteile der neu entwickelten Methode.