Übersetzerverifikation erfordert vor allem für praktische Quell- und
Zielsprachen den Korrektheistnachweis einer großen Menge
Beweisverpflichtungen. Den größten Anteil hieran haben
Implementierungsverifikationen, da auf Ebene der
Implementierungssprache klassische Programmverifikation betrieben
werden muß. Ziel der Programmprüfungsarbeiten im Verifix-Projekt ist
es, diesen Aufwand ganz erheblich zu reduzieren. Der Vortrag zeigt
eine Methode auf, die Gesamtkorrektheit der Implementierung eines
Übersetzers zu etablieren, die auf dem Einsatz korrekt konstruierter
Laufzeitprüfer basiert. Auf die in dem Vortrag von W. Goerigk gelegten
Grundlagen wird Bezug genommen. Im Vortrag zeigen wir in einer
Rechnerdemonstration einen laufenden Übersetzer für unsere
Beispielsprache IS, der durch Anwendung der Programmprüfungsmethode
verifiziert attibutierte Strukturbäume liefert. Der Übersetzer selber
wurde vollständig mit Hilfe der COCKTAIL-Werkzeuge generiert, die
Implementierung liefert eine hocheffiziente Analysephase. In der
Vorführung wird ebenfalls demonstriert, daß fehlerhafte
Implementierungen - hier absichtlich herbeigeführte C- und
Werkzeug-Fehler - sich auf keiner Ebene auf die Gesamtkorrektheit der
Übersetzung auswirken können.