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

Conference Article

[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.


When transforming programs, one often has the requirement to preserve their semantics, as e.g. in compilers. To guarantee that such a requirement is fulfilled, formal proofs are necessary. Therefore, we want to do a simulation proof by showing that the state transitions which appear when running the original and the transformed program, resp., are the same. In a first attempt, one could try an inductive simulation proof over the number of these state transitions. But, as we show here, this approach does not work in general. Induction is fine as long as programs terminate. But for non-terminating programs it is not appropriate. In this paper, we show that a coinductive proof technique is necessary in principle and that the problem of simulation proofs for non-terminating programs can be solved easily using coinduction.

[Generate bibTeX entry]


Prof. Sabine Glesner
Prof. Wolf Zimmermann