Effektive Denotationelle Semantik für die Synthese

• Antragsteller: Professor Dr. Roland Meyer
• Fachliche Zuordnung: Theoretische Informatik ; Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2018 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 417532197

Effektive denotationelle Semantik ist ein aktueller Trend der Verifikation. Gegeben Programm und Spezifikation wird das zugehörige Verifikationsproblem durch Berechnung einer denotationellen Semantik gelöst. Die Semantik wird für das Programm bestimmt aber von der Spezifikation induziert. Die Spezifikation ist typischerweise reaktiv, d.h. sie beschreibt die Interaktion des Programms mit seiner Umgebung. Das vorliegende Projekt wird den Ansatz auf die Programmsynthese verallgemeinern.Anstelle eines Programms nimmt die Synthese nur eine Programmskizze als gegeben an, ein Programm mit Implementierungsalternativen. Gesucht ist eine Vervollständigung der Skizze, die der Spezifikation genügt. Die Vervollständigung fügt der Skizze einen Controller hinzu, der (anhand der Berechnung) Implementierungsalternativen auswählt. Ein Kernproblem der Synthese ist imperfekte Information, die Tatsache, dass Programmund Umgebung den lokale Zustand des anderen nicht sehen. Die existierenden Ansätze zur Synthese unter imperfekter Information sind unzureichend. Die Programmiermodelle sind entweder unentscheidbar oder nicht ausdrucksmächtig. Das vorliegende Projekt konzentriert sich auf die Synthese funktionaler Programme. DieSchlüsselbeobachtung zur Behandlung imperfekter Information ist Folgende. Funktionale Programme haben keinen lokalen Zustand. Die lokale Verarbeitung von Daten geschieht über Choice-Operatoren (Pattern-Matching). Es sind also die Choice-Operatoren, die perfekte oder imperfekte Information über die Berechnung liefern. Wir werden lambda-plus-plus entwickeln (L++), eine funktionale Programmiersprache mit vier Choice-Operatoren (angelic/demonic, perfekt/imperfekt). Mit diesen Operatoren gibt L++ die Trennung zwischen Programm und Umgebung auf. L++ besitzt eine Assertion-Sprache für Spezifikationen. Damit lassen sich Syntheseprobleme als L++-Programme formulieren. L++ soll die Lücke einer ausdrucksmächtigen Programmiersprache mit entscheidbaremSyntheseproblem schließen. Was die Mächtigkeit angeht, werden wir zeigen, dass sichzahlreiche Probleme (der Verifikation, Synthese, Automatentheorie und Graph-Games) als L++-Syntheseprobleme verstehen lassen. Entscheiden werden wir die L++-Synthese mithilfe effektiver denotationeller Semantiken. Diese Semantiken werden auf neuen algebraischen Strukturen beruhen. Die Elemente der Strukturen stellen Berechnungen endlich dar. Die Operatoren dienen der Interpretation von Programmierkonstrukten. Das vorliegende Projekt ist die erste Studie zur denotationellen Semantik imperfekter Information. Die zentralen Ziele des Projekts lauten wie folgt. 1. Löse das Syntheseproblem für das First-Order-Fragment von L++.2. Verstehe die Menge der Vervollständigungen von L++-Programmen.3. Verallgemeinere die Resultate auf das Higher-Order-Fragment von L++.4. Verallgemeinere die Resultate auf unendlichen Speicher.5. Formuliere Probleme anderer Gebiete als L++-Synthese.

• DFG-Verfahren: Sachbeihilfen