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