Der Vortrag gibt einen Überblick über die Definition von Semantiken
mit Abstrakten Zustandsmaschinen (ASMs) und Montages, diskutiert die
Vorgehensweise bei der Verifikation der Transformation, und skizziert
einzelne Simulationsbeweise. Zunächst werden aus den Anforderungen für
Verifix Anforderungen an Semantikstile abgeleitet. Es wird gezeigt,
daß ASMs sehr gut geeignet zur Spezifikation der Semantik von
Maschinensprachen und Zwischensprachen ist, während beispielsweise
denotationale Semantik und strukturell operationale Semantik für
diesen Zweck ungeeignet ist. Da mit Montages eine kompositionale
Spezifikationstechnik zur Definition von ASMs für höhere
Programmiersprachen existiert, sind ASMs eine geeignete
Wahl.Anschließend wird gezeigt, wie man methodisch die Semantiken für
Maschinensprachen, Zwischensprachen und Quellsprachen
definiert. Basierend auf solchen Semantikdefinitionen werden dann die
Transformationen verifiziert. Dazu bildet man zunächst den
Speicherzustandsraum der Quellsprache (Zwischensprache) auf den der
Zwischensprache (Zielsprache) ab, anschließend können die beteiligten
Sprachen vereinigt werden und auf dieser Basis die Transformationen
bewiesen werden, und schließlich wird der Befehlszeiger der
Quellsprache (Zwischensprache) auf den Befehlszeiger der
Zwischensprache (Zielsprache) abgebildet. Der Vortrag zeigt für jeden
dieser Schritte die notwendigen Beweisverpflichtung und führt
exemplarisch solche Beweise vor.