Die meisten der bisher dokumentierten Arbeiten zur maschinell
unterstützten Übersetzer-Spezifikation und -Verifikation betreffen
jeweils spezielle Quell- und Zielsprachen, so dass eine
Wiederverwendung fuer andere Übersetzungsprozesse kaum moeglich
ist. Andrerseits läuft die Übersetzung einzelner Sprachkonstrukte
jeweils nach einem Schema ab, das sich nur in Details von Sprache zu
Sprache unterscheidet; z.B. umfasst die Ubersetzung einer Zuweisung
die Schritte Code-Erzeugung für den Ausdruck, gefolgt von einer
Abspeicherung des berechneten Werts. Es liegt daher nahe, das
Wesentliche solcher Übersetzungsmuster zu identifizieren und abstrakt
zu modellieren und zu verifizieren, so dass sie in geeigneter Form
fuer konkrete Übersetzungsprozesse instanziiert und wiederverwendet
werden können. Ein solches Vorgehen unterstuetzt ausserdem die fuer
die Durchfuehrbarkeit maschineller Beweise notwendige Modularisierung
des Übersetzungsprozesses. In dem Vortrag werden beispielhaft
generische Theorien zur Übersetzung von Ausdruecken und darauf
aufbauend fuer Kontrollstrukturen vorgestellt, die von Details der
Quellsprache und Architektur und Instruktionssatz der Zielmaschine
abstrahieren. Wir zeigen, wie und in welchem Umfang ein solchen Ansatz
sich im PVS-System realisieren lässt und wie die abstrakten Theorien
für die konkreten Übersetzungsprozesse des Verifix-Projektes
eingesetzt werden können.