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