Motivation für die Forschung
Die inhärente theoretische Komplexität des Problems der Softwaresynthese sowie die pragmatische Komplexität des Schreibens und Verstehens von Softwarespezifikationen sind die größten Herausforderungen bei der Reduzierung der Softwaresynthese auf die Praxis. Ein Ansatz, um einen Teil dieser Komplexität zu vermeiden, ist die komponentenorientierte Synthese, bei der im Gegensatz zum traditionellen Ansatz, bei dem die Synthese von Grund auf erfolgt, Systeme durch das Zusammenfügen von Komponenten aus einem bestimmten Repository, das für einen sehr spezifischen Anwendungskontext entwickelt wurde, zusammengestellt werden. Obwohl der komponentenbasierte Ansatz die Wiederverwendbarkeit verbessert und die Strukturierung von Software erleichtert, nimmt die eigentliche Aufgabe des Abrufens, Konfigurierens und Zusammenfügens der geeigneten Komponenten unverhältnismäßig viel Zeit bei der Realisierung eines Softwareprodukts in Anspruch. Hier ist ein hoher Grad an Automatisierung wünschenswert.
Auf einer allgemeineren Ebene ist das Syntheseproblem (Alonzo Church, 1957), d.h. das Problem der automatischen Generierung eines Programms oder Systems, das eine gegebene Spezifikation erfüllt, von grundlegender Bedeutung für die (theoretische) Informatik. Es gibt eine Reihe von Ergebnissen zur automatischen Synthese, die jedoch aufgrund der oben erwähnten pragmatischen Komplexität nicht für die Synthese von Software in der realen Welt geeignet sind.
Die Motivation hinter den Forschungsarbeiten bei SEAL ist die Anwendung der jüngsten Grundlagenforschung zum Syntheseproblem auf der Basis der Typentheorie auf die Software-Synthese aus einem Repository von Komponenten. Der typbasierte Ansatz ist naheliegend, da die Typentheorie von Natur aus komponentenorientiert ist und Komponenten durch ihre Schnittstellen auf natürliche Weise Typen aufweisen. Wenn man sich außerdem darauf verlässt, dass die Komponenten korrekt spezifiziert sind, werden Spezifikationen für komplexe Software viel einfacher (eben weil nicht alles von Grund auf neu spezifiziert werden muss). Wir verwenden Schnittstellentypen (Coppo-Dezani-Sallé-Typen), um die Schnittstellen der Implementierungssprachen (d.h. die nativen Ein- und Ausgabetypen der Komponenten) mit semantischen Informationen anzureichern. Dies ermöglicht eine intuitive Art und Weise der Spezifikation von Softwarekomponenten, da eine Komponente mit Hilfe von Konzepten in einem nahezu beliebigen Detaillierungsgrad beschrieben werden kann. Die daraus resultierende Spezifikationslogik (kombinatorische Logik) ist einfach, aber enorm aussagekräftig. Wir haben verschiedene typentheoretische Ergebnisse zur kombinatorischen Logik mit Schnittpunkttypen verwendet, um einen leistungsfähigen Rahmen für die automatische Komposition von Komponenten zu implementieren, der auf einem automatischen Theorembeweiser für kombinatorische Logik basiert.
Translated with DeepL