Universität Karlsruhe
Structural Simulation Proofs based on ASMs even for Non-Terminating Programs

Konferenzartikel

[zwingend]Sabine Glesner, Wolf Zimmermann, Structural Simulation Proofs based on ASMs even for Non-Terminating Programs, Proceedings of the ASM-Workshop, Eight International Conference on Computer Aided Systems Theory EUROCAST 2001, Feb 2001.

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. 

[Erzeuge bibTeX Eintrag]

Autoren

Alumni
Prof. Sabine Glesner
Prof. Wolf Zimmermann
Login
Links