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

    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.