Automatischer Korrektheitsnachweis von Programmtransformationen
Final Report Abstract
Im DFG-Projekt „Automatischer Korrektheitsnachweis von Programmtransformationen“ werden die Möglichkeiten zur Automatisierung der Korrektheitsbeweise von Programmtransformationen im Rahmen der Theorie der kontextuellen Gleichheit untersucht und ein Tool (Aucopro) zum automatischen Korrektheitsbeweis entwickelt. Dazu werden (call-by-need) Programmkalküle mit einer operationalen Semantik in Form von Reduktionsregeln und einer Definition der kontextuellen Gleichheit betrachtet. Die wesentlichen Schritte, die zur Automatisierung in solchen Kalkülen unternommen werden müssen, sind einerseits die Berechnung vollständiger Diagrammmengen, die sich gliedert in die Bestimmung von Überlappungen zwischen Reduktionsregeln der Programmkalküle und deren anschließende Zusammenführung; sowie andererseits eine Automatisierung des induktiven Teils der Korrektheitsbeweise unter Verwendung der zuvor berechneten Diagramme. Die wesentlichen Resultate, die dazu in den bisherigen Arbeiten erzielt wurden, sind: • Es wurde eine Meta-Sprache zur Darstellung von Lambda-Kalkülen mit letrec entworfen. • Es wurden Unifikationsalgorithmen (aufbauend auf der Meta-Sprache) zur Überlappungsberechnung von Transformationen und Standardreduktion in den beiden ausdrucksstarken Lambda-Kalkülen LN und LR entworfen. Für diese wurde der Nachweis ihrer wesentlichen Eigenschaften erbracht, so dass die Berechnung aller Überlappungen sicherstellt ist: Vollständigkeit, Korrektheit, Terminierung und endlicher Unifikationstyp. • Zum Schließen von Überlappungen wurden Algorithmen entwickelt und untersucht, insbesondere im Hinblick auf die Komplexität des Tests auf erweiterte α-Äquivalenz, der notwendig ist um festzustellen, ob Diagramme geschlossen sind. • Es wurden Algorithmen und Kodierungen entwickelt, die zu einer Programmtransformation und deren vollständiger Menge von Diagrammen automatisch die Korrektheit der Programmtransformation zeigen können. • Das Tool Aucopro wurde entwickelt, das die theoretischen Konzepte zum automatischen Korrektheitsnachweis implementiert. Es stellt somit ein „Proof of Concept“ der entwickelten Theorien dar, indem es praktisch in der Lage ist (unter bestimmten Voraussetzung) die Korrektheit von Programmtransformationen automatisch zu zeigen. Diese Resultate erlauben den Schluss, dass es in dem gegebenen theoretischen Rahmen (callby-need Kalküle mit explizitem sharing und kontextueller Semantik) und unter bestimmten Voraussetzung möglich ist, die Korrektheit von Programmtransformationen automatisch zu beweisen.
Publications
- Correctness of Program Transformations as a Termination Problem. In: In Gramlich, B., Miller, D., and Sattler, U., (Hrsg.): Automated Reasoning - Proceedings of the 6th International Joint Conference (IJCAR 2012). Bd. 7364 Lecture Notes in Computer Science, S. 462-476, Springer Berlin / Heidelberg, 2012
Rau, C., Sabel, D., Schmidt-Schauss, M.
- Algorithms for Extended Alpha- Equivalence and Complexity. In: Raamsdonk, F. van (Hrsg.): 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Bd. 21. Leibniz International Proceedings in Informatics (LIPIcs), S. 255-270, Dagstuhl, Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2013
Schmidt-Schauss, M., Rau, C., Sabel, D.
