Mechanical verification of total correctness through diversion verification conditions
The total correctness of programs with mutually recursive procedures is significantly more complex than their partial correctness. Past methods of proving termination have suffered from being rigid, not general, non-intuitive, and ad hoc in structure, not suitable for mechanization. We have devised a new method for proving termination and mechanized it within an automatic tool called a Verification Condition Generator. This tool analyzes not only the program's syntax but also, uniquely, its procedure call graph, to produce verification conditions sufficient to ensure the program's total correctness. Diversion verification conditions reduce the labor involved in proving termination from infinite to finite. The VCG tool has itself been deeply embedded and proven sound within the HOL theorem prover with respect to the underlying structural operational semantics. Now proofs of total correctness of individual programs may be significantly automated with complete security.
KeywordsProcedure Call Recursive Procedure Path Condition Verification Condition High Order Logic
Unable to display preview. Download preview PDF.
- 3.M. Gordon and T. Melham. Introduction to HOL, A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, 1993.Google Scholar
- 4.C. A. R. Hoare. Procedures and Parameters: an axiomatic approach. In: Proceedings of Symposium on Semantics of Algorithmic Languages, ed. E. Engeler, volume 188 of Lecture Notes in Mathematics, pages 102–116, 1971.Google Scholar
- 5.P. Homeier. Trustworthy Tools for Trustworthy Programs: A Mechanically Verified Verification Condition Generator for the Total Correctness of Procedures. Ph.D. Dissertation, UCLA Computer Science Department, 1995.Google Scholar
- 7.P. Homeier and D. Martin. Mechanical Verification of Mutually Recursive Procedures. In M. A. McRobbie and J. K. Slaney (eds.), Proceedings of the 13th International Conference on Automated Deduction (CADE-13), volume 1104 of Lecture Notes in Artificial Intelligence, pages 201–215, Springer-Verlag, 1996.Google Scholar
- 9.T. Melham. A Package for Inductive Relation Definitions in HOL. In M. Archer, J. Joyce, K. Levitt, and Windley (eds.), Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991. IEEE Computer Society Press, pages 350–357, 1992.Google Scholar
- 11.S. Sokolowski. Total Correctness for Procedures, In J. Gruska (ed), Proceedings, 6th Symposium on the Mathematical Foundations of Computer Science, volume 53 of Lecture Notes in Computer Science, pages 475–483, Springer-Verlag, 1977.Google Scholar