| 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.
|
ZusammenfassungBeim 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.
Autoren
| |
