Vorlesung Gliederung Kommentar Übungen Univis  

Probleme beim Bau voll korrekter Übersetzer, WS 2004 / 05 (080085)
 
Vorlesung, 4 SWS, Schein, ECTS-Studium, ECTS-Credits: 4,0, Fachgebiet: Praktische Informatik
Zeit und Ort: Di, Mi 16 - 18 c.t., Raum wird noch bekanntgegeben
Erster Termin: Di 19. 10. 2004

Dozent
PD Dr. Wolfgang Goerigk

Verweise
Übungen zur Vorlesung Probleme beim Bau voll korrekter Übersetzer

Gliederung
  1. Einführung und Begriffe
  1. Historisches, Einordnung
  2. Phasen eines Übersetzers
      (lexikalische, syntaktische, statisch semantische Analyse; Transformation; Codegenerierung)
  3. Sequentielle transformationelle Programmiersprachen, Semantik
  4. Maschinensprachen, Semantik
  5. Übersetzungen, Übersetzungskorrektheit
  6. Programmkorrektheit, Erhalten von Programmkorrektheit
   2. Ein konkreter Übersetzer
  7. Zielmaschine, Zielcode
  8. Quellsprache
  9. Übersetzungsspezifikation, Übersetzerimplementierung
10. Übersetzerbootstrapping, starker Übersetzertest
   3. Übersetzerimplementierung und Trojanische Pferde
11. Selbstreproduzierende Programme, reflektive Programme
12. Bedingte Selbstreproduktion
13. Bedingt selbstreproduzierende Übersetzer
14. Eine heimtückische Übersetzerimplementierung
   4. Volle Übersetzerimplementierungsverifikation
15. Übersetzungskorrektheit
16. Korrekte Übersetzerimplementierung
17. Korrektheit der Übersetzerkonstruktion, Daten- und Operationsverfeinerung
18. Korrektheit der Übersetzermaschinenimplementierung
      - Spezielles Bootstrapping
      - Syntaktischer a-posteriori-Code-Vergleich
19. Diagonalverfahren bei Mehrphasenübersetzung
   5. Fortgeschrittene Implementierungs- und Beweistechniken
20. Einsatz von Übersetzergeneratoren
21. Verifizierte Ergebnisprüfung (runtime result verification)

Kommentar
Übersetzer werden als Werkzeuge an zentraler Stelle im Software-Entwicklungsprozess eingesetzt. Die Zuverlässigkeit und Sicherheit von Software hängt auch von der Korrektheit der zur Implementierung herangezogenen Übersetzerprogramme ab. Um korrekte Übersetzer zu entwerfen und schließlich korrekt auf der Maschine zu implementieren - zur Konstruktion voll korrekter Übersetzer - müssen sowohl die Korrektheit der Transformation (Übersetzungskorrektheit) als auch die der Implementierung des Übersetzers auf allen Ebenen bis hinab zum ablaufenden Maschinencode lückenlos nachgewiesen werden. Übersetzungsverifikation blickt bereits auf eine über 30jährige Tradition zurück. Übersetzer führen syntaktische Transformationen von Quell- in Zielprogramme durch, die die Semantiken von Quell- und Zielsprache zu respektieren haben. Adäquate Semantikdefinitionsstile für höhere Quellsprachen und maschinennahe Zielsprachen, verschiedene Korrektheitsbegriffe für Compiler sowie Methoden für den Korrektheitsnachweis (die Übersetzungsverifikation) werden im ersten Teil der Vorlesung studiert, vor allem mit Blick auf praktische Durchführbarkeit der Beweise und praktischen Nutzen der bewiesenen Eigenschaften.

Es ist möglich, Programme zu schreiben, die sich selbst reproduzieren, auch Übersetzer, die ihre eigene - z.B. absichtlich durch ein Trojanisches Pferd infizierte - Maschinencodeimplementierung reproduzieren, wenn sie zur Implementierung (zum Bootstrapping) ihres eigenen Quellcodes ausgeführt werden. Solche Programme können in speziellen Situationen oder für spezielle Eingaben, die nur dem Infizierer bekannt sind, katastrophale Auswirkungen haben, sind im Bereich der IT-Sicherheit (engl. security) untragbar. Absichtlich sehr versteckte Fehler werden durch Testen kaum gefunden werden. Wir werden im zweiten Teil einen solchen (sogar im Quellcode verifizierten) Übersetzer kennenlernen, der für alle bis auf zwei Quellprogramme höchstens korrekten Zielcode generiert, und der zudem, obwohl er falsch ist, den von Übersetzerbauern hochgeschätzten Wirth'schen strengen Übersetzertest besteht.

Im dritten Teil widmen wir uns der lückenlosen Verifikation der Übersetzerimplementierung, so daß jedweder Fehler, auch absichtliche wie Viren oder Trojanische Pferde, garantiert ausgeschlossen werden kann. Wir werden Methoden zur korrekten Programmkonstruktion und die Technik der a-posteriori-Programmprüfung studieren, mit der große Teile zu verifizierender Programme durch spezielle Überprüfungen abgesichert werden können. Eine spezielle Bootstrap-Technik mit nachträglicher Codeinspektion erlaubt den Nachweis der Korrektheit niederer Übersetzerimplementierungen mit weitgehender maschineller Unterstützung, ohne erneut in Abhängigkeit von unverifizierter Software zu geraten.

Die Vorlesung wendet sich an Hauptfach-Informatikstudenten nach dem Vordiplom. Kenntnisse in Übersetzerbau, Semantik von Programmiersprachen oder Programmverifikation sind von Vorteil, werden aber nicht vorausgesetzt.

Empfohlene Literatur
Aho, Ullman: The Theory of Parsing, Translation and Compiling I, II. Prentice-Hall, 1973.
Gries: Compiler Construction for Digital Computers. Wiley, 1971.
Alagic, Arbib: The Design of Well Structured and Correct Programs. Springer, 1978.
Moore: Piton. A Mechanically Verified Assembly-Level Language. Kluver Academic Publishers, 1996.
Allan: The Anatomy of Lisp.
Loeckx, Sieber: The Foundations of Program Verification. Wiley-Teubner, 1984.
Müller-Olm: Modular Compiler Verification. Springer LNCS 1283, 1997
Auf weitere Literatur wird jeweils in der Vorlesung hingewiesen.