Bei der Entwicklung verifizierter Übersetzer fallen eine Vielzahl von
Modellierungs-, Spezifikations- und Beweisaufgaben an, die ohne
maschinelle Unterstützung nur schwer zu bewältigen sind, wenn der
Anspruch auf formal begründete und nachvollziehbare Schritte erfüllt
werden soll. Es ist ein formal-logischer Rahmen erforderlich, der
einerseits die für die Modellierung von Sprachen und Zielmaschinen und
deren Semantik notwendige Ausdruckskraft bereitstellt, andrerseits
auch genügende Unterstützung für deren Analyse, insbesondere die
Entwicklung formaler Beweise, bietet, so dass die gesamte formale
Entwicklung in einem einheitlichen, maschinell gestützten logischen
Kontext geschieht. Aus pragmatischen Gründen wird im Verifix-Projekt
für diese Aufgabe PVS eingesetzt. Anhand von typischen Beispielen
illustrieren wir Modellierung und Beweis in PVS und zeigen, inwieweit
PVS den Anforderungen gerecht wird, die sich bei der Entwicklung
verifizierter Übersetzer ergeben.