Formalizing Hoare Logic in PVS
We formalize a Hoare logic for the partial correctness of while programs in PVS and prove its soundness and relative completeness. We use the PVS higher-order logic to define the syntax and semantics of a small imperative programming language, and describe a proof system for Hoare triples involving programs in this language. We prove the soundness of the proof system by demonstrating that only valid triples are provable. We also demonstrate the relative completeness of the proof system by defining the weakest liberal precondition operator and using it to prove that all valid Hoare triples are provable modulo the assertion logic. Finally, we verify a verification condition generator for Hoare logic Variants of Hoare logic have been formalized before in PVS and using other interactive proof assistants. We use Hoare logic as a tutorial exercise to illustrate the effective use of PVS in capturing the syntax and semantics of embedded logics. The embedding of Hoare logic is simple enough to be easily reproduced by the reader, but it also illustrates some of the nuances of formalization and proof using PVS, in particular, and higher-order logic, in general.
The author is grateful to Zhiming Liu for his excellent organization of the SETTS 2017 school, to Jonathan Bowen for his patient editing, and to the anonymous referees for their insightful comments and helpful suggestions for improving the paper. This work was funded by DARPA under agreement number FA8750-16-C-0043. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of DARPA or the U.S. Government.
- 3.Archer, M., Heitmeyer, C.: Mechanical verification of timed automata: a case study. In: IEEE Real-Time Technology and Applications Symposium (RTAS 1996), Brookline, MA, June 1996, pp. 192–203. IEEE Computer Society (1996)Google Scholar
- 7.de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparrison. Cambridge Tracts in Theoretical Computer Science, vol. 47. Cambridge University Presss (1998)Google Scholar
- 8.Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, vol. XIX, pp. 19–32. American Mathematical Society, Providence (1967)Google Scholar
- 9.Gordon, M.J.C.: Mechanizing programming logics in higher order logic. Technical Report CCSRC-006, SRI International, Cambridge Computer Science Research Centre, Suite 23, Millers Yard, Mill Lane, Cambridge CB2 1RQ, England, September 1988Google Scholar
- 10.Hensel, U., Huisman, M., Jacobs, B., Tews, H.: Reasoning about classes in object-oriented languages: logical models and tools. Technical Report CSI-R9718, Computing Sciences Institute, Katholieke Universiteit Nijmegen, Nijmegen, The Netherlands, October 1997Google Scholar
- 12.Jackson, D.: Automating first-order relational logic. In: Proceedings of ACM SIGSOFT Conference on Foundations of Software Engineering, November 2000Google Scholar
- 13.McCarthy, J.: Towards a mathematical science of computation. In: Proceedings of IFIP Congress, pp. 21–28. North-Holland (1962)Google Scholar
- 17.Muñoz, C.: PBS: support for the B-method in PVS. Technical Report SRI-CSL-99-1, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1999Google Scholar
- 18.von Neumann, J., Goldstine, H.H.: Planning and coding of problems for an electronic computing instrument. Institute for Advanced Study, Princeton, New Jersey (1948). Reprinted in Google Scholar
- 21.Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: prolegomena to the design of PVS. IEEE Trans. Softw. Eng. 21(2), 107–125 (1995). PVS home page: http://pvs.csl.sri.com
- 22.Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)Google Scholar