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

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.