Proof Styles in Operational Semantics

S. Ray and J S. Moore

Draft, December 2003.

Abstract

We relate two well-studied methodologies, use of inductive invariants and clock functions, in deductive verification of operationally modeled sequential programs. We prove that the two methodologies are equivalent in the following sense: If the logic used is sufficiently expressive then one can mechanically transform a proof of a program in one methodology to a proof in the other. Both partial and total correctness are considered in this context. We also show that the mechanical transformation is compositional in that different parts of a program can be verified using different methodologies to achieve a complete proof of the entire program. Our proof of equivalence has been mechanically verified by the ACL2 theorem prover and we discuss automatic tools in the form of ACL2 macros to carry out the mechanical transformation between the two methodologies in the context of ACL2 theorem proving.

Relevant files