Übersetzer Codegeneratoren übersetzen Programme aus niedrigen
Zwischensprachen in äquivalente Maschinenprogramme. Wir definieren die
Korrektheit dieser Übersetzung basierend auf operationalen Semantiken
der Zwischen- und Maschinensprache, wobei die
Übersetzungsspezifikation durch eine Menge von Termersetzungsregeln
gegeben ist. Der Vortrag zeigt, daß alle Codegeneratoren, die durch
ein Termersetzungssystem erzeugt wurden, korrekt sind, wenn der
Codegenerator-Generator, Registerzuteiler, sowie die
Termersetzungsregeln bestimmten Anforderungen genügen. Die
Anforderungen an die einzelnen Termersetzungsregeln sind unabhängig
von den restlichen Termersetzungsregeln und bestehen aus
Einzelsimulationen, die zu einem Simulationsbeweis zusammengesetzt
werden können. Die Korrektheit des Codegenerator-Generators und die
Anforderungen an den Registerzuteiler sind unabhängig von den
beteiligten Sprachen und sind nur mit Zwischensprache und
Maschinensprache parametrisiert. Zur Konstruktion korrekter Übersetzer
genügt es demnach, diese beiden Aufgaben insgesamt aus einer korrekten
Bibliothek zu entnehmen, die für alle Codegeneratoren verwendet werden
kann. Um einen neuen korrekten Codegenerator zu konstruieren, reicht
es aus die Anforderungen an die einzelnen Termersetzungsregeln zu
beweisen und den Codegenerator-Generator und Registerzuteiler aus der
Bibliothek geeignet zu parametrisieren. Der Vortrag von T. Gaul führt
anhand einzelner Beispiel solche Beweise durch.