A Problem-Reduction Approach to Proving Simulation Between Programs

Abstract

System correctness often presents itself as the problem of showing that two programs, the “specification” and the “implementation,” are in some sense equivalent. Such a concept of equivalence is supplied by Milner's definition of simulation between programs. This paper presents a problem-reduction approach to proving simulation, and describes an interactive system designed for this purpose. The main feature of our approach is an integrated structure for the entire problem of proving simulation. This is achieved by unifying various steps, such as generation of verification conditions, simplification, and theorem proving, into a uniform process of goal decomposition starting from the initial goal of proving simulation between two programs. This approach facilitates user interaction by giving him a better view of the entire proof, and thus improves error detection when parts of the proof fail. An example of a simulation proof involving simulation between two flow-chart programs illustrates the use of the system, which has also been used in verifying microprograms. Copyright © 1976 by The Institute of Electrical and Electronics Engineers, Inc.