Am Beispiel der verifizierten Übersetzung einer einfachen
While-Sprache stellen wir eine Instanziierung der Architektur zur
Konstruktion verifizierter Übersetzer vor. Die Zielsprache ist dabei
eine Teilmenge des DecAlpha Maschinenkodes. Es zeigt sich, daß die
Übersetzungsspezifikation auf natürliche Art und Weise entsprechend
der traditionellen Übersetzerstruktur aufgeteilt werden kann. Eine
weitere Verfeinerung der Spezifikation und Implementierung führt zu
Modulen, die für jeden Übersetzer, die nur ein einziges Mal oder die
überhaupt nicht verifiziert werden müssen. Trotz der einfachen Quell-
und Zielsprache behandelt die Übersetzung viele praktisch relevante
Probleme, z.B. wird explizit eine Zwischensprache eingeführt und es
wird auf die Korrektheit der Registerallokation und der Adressrechnung
eingegangen.