Vorlesung
Gliederung
Kommentar

Übungen
 

 Probleme beim Bau voll korrekter Übersetzer, SS 2001
  PD Dr. Wolfgang Goerigk, DI, DO 16 - 18 Uhr, CAP3-1
 
---
 
Vorlesung, 4 SWS, Schein, ECTS-Studium, ECTS-Credits: 6,0, Fachgebiet: Praktische Informatik
Zeit und Ort: Di, Do 16:00 - 18:00 c.t., Raum CAP3-1
Erster Termin: 17. 4. 2001, 16:00 - 18:00 Uhr c.t.
---

Verweise

  • Auszug aus dem  Informationssystem der Universität Kiel - Semester: SS 2001
  • Übungen zur Vorlesung Probleme beim Bau voll korrekter Übersetzer
  • Gliederung

      I. 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
      II. Ein konkreter Übersetzer
        7. Zielmaschine, Zielcode
        8. Quellsprache
        9. Übersetzungsspezifikation, Übersetzerimplementierung
      10. Übersetzerbootstrapping, starker Übersetzertest
      III. Übersetzerimplementierung und Trojanische Pferde
      11. Selbstreproduzierende Programme, reflektive Programme
      12. Bedingte Selbstreproduktion
      13. Bedingt selbstreproduzierende Übersetzer
      14. Eine heimtückische Übersetzerimplementierung
      IV. 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
      V. 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.