Proof Styles in Operational Semantics
S. Ray and J S. Moore
Draft, December 2003.
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.
- Paper (ps, pdf)
- Supporting ACL2 proof
scripts: See the directory
the current ACL2 distribution.