Der Vortrag diskutiert den Zusammenhang zwischen der operationellen
Semantikspezifikation von Quellsprachen mit Montages und den
Beweisverpflichtungen zum Nachweis der Korrektheit von
Übersetzungen. Wir geben eine Konstruktionsmethode an, mit der aus dem
Nachweis der lokalen Korrektheit von Übersetzungen von Sprachkonzepten
auf die globale Korrektheit geschlossen werden kann. Damit ergibt sich
eine Modularisierung des Korrektheitsbeweises für die
Transformationsphase. Zusätzlich diskutieren wir
Wiederverwendungsfragen und stellen einen Kalkül für korrekte
Übersetzungen vor. Der Kalkül stellt im Prinzip eine Bibliothek von
Sprachkonzepten zusammen mit korrekten Übersetzungen dar. Definiert
man die Semantik einer Quellsprache durch Abbildung in die Sprache des
Kalküls, dann können sowohl Semantik von Sprachkonzepten als auch
korrekte Transformationen wiederverwendet werden. Der Kalkül ist durch
eine objekt-orientierte Bibliothek
implementiert. Implementierungskorrektheit ergibt sich durch korrekte
Komposition von beschränkten generischen Klassen, die Sprachkonzepte
repräsentieren, und Standardprogrammverifikation von Transformationen.