direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Publikationen

Structural Simulation Proofs based on ASMs even for Non-Terminating Programs
Zitatschlüssel GlesnerZimmermannASM2001
Autor Sabine Glesner and Wolf Zimmermann
Buchtitel Proceedings of the ASM-Workshop, Eight International Conference on Computer Aided Systems Theory EUROCAST 2001
Seiten 235-238
Jahr 2001
Adresse IUCTC Universidad de Las Palmas de Gran Canaria, Spain
Zusammenfassung Beim Transformieren von Programmen, wie z.B. in Übersetzern, muss man häufig deren Semantik erhalten. Um eine solche Anforderung formal zu garantieren, sind formale Beweise erforderlich. Man will deshalb Simulationsbeweise durchführen, die zeigen, dass die Zustandsübergänge, die im ursprünglichen Programm durchlaufen werden, dieselben sind wie im transformierten Programm. In einem ersten Anlauf könnte man versuchen, das durch einen induktiven Beweis über die Anzahl der Zustandsübergänge nachzuweisen. Aber dieser Ansatz ist, wie wir hier zeigen, im allgemeinen Fall nicht anwendbar. Denn Induktion ist nur solange anwendbar, wie die betrachteten Programme terminieren. Für nicht-terminierende Programme brauchen wir koinduktive Beweistechniken, mit denen derartige Simulationsbeweise leicht geführt werden können.
Typ der Publikation Conference Article
Download Bibtex Eintrag

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe