Universität Karlsruhe
Structural Simulation Proofs based on ASMs even for Non-Terminating Programs
@conference{zwingend,
  author={Sabine Glesner and Wolf Zimmermann},
  title=\{Structural Simulation Proofs based on ASMs even for Non-Terminating Programs},
  booktitle=\{Proceedings of the ASM-Workshop, Eight International Conference on Computer Aided Systems Theory EUROCAST 2001},
  year=\{2001},
  month=\{Feb},
  abstract=\{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. },
}

Login
Links