Die Vorlesung setzt Grundkenntnisse des Übersetzerbaus, etwa aus der Vorlesung Übersetzerbau, voraus. Empfehlenswert ist auch der vorige Besuch der Vorlesung "Weiterführender Übersetzerbau". 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.
Die Vorlesung wird im Rahmen einer ERASMUS/LLP-Vereinbarung zwischen der TU Wien und der Martin-Luther-Universität Halle-Wittenberg, Deutschland, von Professor Dr. habil. Wolf Zimmermann als Blockveranstaltung in der Zeit vom 01.03.2011 bis zum 11.03.2011 gehalten. Die Vorbesprechung zur Lehrveranstaltung findet zum ersten Veranstaltungstermin am 01.03.2011 um 16:00 Uhr statt. Der Veranstaltungsort ist die Bibliothek des Arbeitsbereichs für Programmiersprachen und Übersetzer in der Argentinierstr. 8, 4. Stock (Mitte), 1040 Wien.
Nicht erforderlich
Vorkenntnisse aus dem Übersetzerbau etwa in dem in den LVAs 185.311 (und 185.274) vermittelten Umfang sind wünschenswert.
