Advertisement

Formalizing Hoare Logic in PVS

  • Natarajan ShankarEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11174)

Abstract

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.

Notes

Acknowledgments

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.

References

  1. 1.
    Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefGoogle Scholar
  2. 2.
    Apt, K.R.: Ten years of Hoare’s logic: a survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)CrossRefGoogle Scholar
  3. 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
  4. 4.
    Bentley, J.L.: Programming pearls: algorithm design techniques. Commun. ACM 27(9), 865–871 (1984)CrossRefGoogle Scholar
  5. 5.
    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Heidelberg (2018).  https://doi.org/10.1007/978-3-319-10575-8CrossRefzbMATHGoogle Scholar
  6. 6.
    Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70–90 (1978)MathSciNetCrossRefGoogle Scholar
  7. 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. 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. 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. 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
  11. 11.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12(10), 576–583 (1969)CrossRefGoogle Scholar
  12. 12.
    Jackson, D.: Automating first-order relational logic. In: Proceedings of ACM SIGSOFT Conference on Foundations of Software Engineering, November 2000Google Scholar
  13. 13.
    McCarthy, J.: Towards a mathematical science of computation. In: Proceedings of IFIP Congress, pp. 21–28. North-Holland (1962)Google Scholar
  14. 14.
    McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Technical Monographs in Computer Science. Springer, New York (2005).  https://doi.org/10.1007/b138392CrossRefzbMATHGoogle Scholar
  15. 15.
    Morris, F.L., Jones, C.B.: An early program proof by Alan Turing. IEEE Ann. Hist. Comput. 6, 139–143 (1984)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Moscato, M.M., Pombo, C.L., Frias, M.F.: Dynamite: a tool for the verification of Alloy models based on PVS. ACM Trans. Softw. Eng. Methodol 23(2), 20:1–20:37 (2014)CrossRefGoogle Scholar
  17. 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. 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 [25]Google Scholar
  19. 19.
    Nipkow, T., Klein, G.: Concrete Semantics - With Isabelle/HOL. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-319-10542-0CrossRefzbMATHGoogle Scholar
  20. 20.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55602-8_217CrossRefGoogle Scholar
  21. 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. 22.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)Google Scholar
  23. 23.
    Shankar, N.: Combining Model Checking and Deduction. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 651–684. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-10575-8_20CrossRefzbMATHGoogle Scholar
  24. 24.
    Skakkebæk, J.U., Shankar, N.: Towards a duration calculus proof assistant in PVS. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 660–679. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58468-4_189Google Scholar
  25. 25.
    von Neumann, J.: Collected Works, vol. V. Pergamon Press, Oxford (1961)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Computer Science LaboratorySRI InternationalMenlo ParkUSA

Personalised recommendations