An Algebraic Definition of Simulation Between Programs. AIM-142

A simulation relation between programs is defined which is
quasi-ordering. Mutual simulation is then an equivalence relation,
and by dividing out by it we abstract from a program such details as
how the sequencing is controlled and how data is represented. The
equivalence classes are approximations to the algorithms which are
realized, or expressed, by their member programs.

A technique is given and illustrated for proving simulation and
equivalence of programs; there is an analogy with Floyd's technique
for proving correctness of programs. Finally, necessary and
sufficient conditions for simulation are given.