On homomorphisms, simulations,correctness and subroutines for programs and program schemes

Abstract

This paper presents a definition of homomorphism for programs and applies it to giving simplified proofs of correctness, equivalence, termination, and other properties of programs. We mean "simplified" in the sense that no manipulations with first (or higher) order logic, or other formal systems, are required, and that human beings can often produce shorter and more systematic (rigorous) proofs than by other methods. We use only the most elementary set theory for verifying programs, although some fancier algebra is needed for program schemes. This paper emphasizes the proofs of the validity of the verification methods for programs, and this does use some elementary category theory. But we also include a number of examples to illustrate the power of the methods. These also serve as an expository device for the more difficult theory of verification for program schemes.