Diese Veranstaltung ist eine Vorlesung kombiniert mit einem Seminar. In der ersten Hälfte des Semesters findet eine Vorlesung mit den unten stehenden Zielen statt. In der zweiten Hälfte des Semesters wird in Form eines Seminars über ausgewählte Arbeiten aus diesem Gebiet referiert.
Lernziele:
* Kenntnis der Methoden der Übersetzerverifikation
* An Hand einfacher Beispiele selbstständig Übersetzer verifizieren können.
Die Vorlesung setzt Grundkenntnisse des Übersetzerbaus, etwa aus der
Vorlesung Übersetzerbau, voraus. Empfehlenswert ist auch der vorige
Besuch der Vorlesung "Weiterführender Übersetzerbau".
Inhalt:
Bei sicherheitskritischen Anwendungen dürfen oft nur einfachste
Übersetzer verwendet werden bzw. müssen direkt in Maschinensprache
programmiert werden. Ursache hierfür ist mangelndes Vertrauen in die
korrekte Funktionsweise von Übersetzern. In der Tat gibt es bei
ausgelieferten Übersetzern so viele Fehler, dass durch die Verwendung
handelsüblicher oder öffentlicher Übersetzer oft nicht die notwendige
Zuverlässigkeit sicherheitskritischer Anwendungen erreicht werden kann.
Das Thema dieser Vorlesung behandelten Methoden sollten zukünftig den
Einsatz optimierender Übersetzer auch im sicherheitskritischen Bereich
ermöglichen. Die Methoden und Vorgehensweisen orientieren sich an den im
Projekt Verifix erarbeiteten Resultate.
In der Vorlesung wird an Hand einer einfachen Programmiersprache die
Konstruktion eines korrekten Übersetzers demonstriert. Korrektheit heißt
im weiteren Sinne, dass der vom Übersetzer erzeugte Code die Semantik
des zu übersetzenden Programms erhält. Dazu ist es zunächst notwendig,
aufzuzeigen, wie man eine formale Semantik einer Programmiersprache
definieren kann (wir verwenden hier abstrakte Zustandsmaschinen).
Anschließend wird für jede der einzelnen Übersetzerschritte gezeigt, wie
man deren Korrektheit nachweist. Man unterscheidet die Verifikation der
Transformationsregeln (Erhaltung der Semantik) und deren Implementierung
im Übersetzer. Für Ersteres verwendet man eine Technik ähnlich den
Simulationsbeweisen aus der Komplexitäts- und Berechenbarkeitstheorie,
für Letzteres wird für jeden Übersetzeraufruf überprüft, ob die
Transformationsregeln korrekt angewendet wurden. Nur mit beidem zusammen
kann man die Korrektheit von Übersetzern sicherstellen.
Aufbau der Vorlesung:
1. Einleitung (Was heißt Korrektheit von Übersetzern?)
2. Grundlagen und Semantik von Programmiersprachen
3. Korrektheit der Speicherabbildung
4. Korrektheit der Zwischencodeeerzeugung
5. Korrektheit der Codeerzeugung und der Assemblierung
