Skip to main content
SpringerLink
Log in

Weakest Precondition for General Recursive Programs Formalized in Coq

  • Conference paper
  • First Online:
Theorem Proving in Higher Order Logics (TPHOLs 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2410))

Included in the following conference series:

Abstract

This paper describes a formalization of the weakest precondition, wp, for general recursive programs using the type-theoretical proof assistant Coq. The formalization is a deep embedding using the computational power intrinsic to type theory. Since Coq accepts only structural recursive functions, the computational embedding of general recursive programs is non-trivial. To justify the embedding, an operational semantics is defined and the equivalence between wp and the operational semantics is proved. Three major healthiness conditions, namely: Strictness, Monotonicity and Conjunctivity are proved as well.

The work in this paper is sponsored by the EPSRC project GUSTT.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. J. R. Back. A calculus of refinements for program derivations. Acta Informatica, 25(6):593–624, August 1988.

    Google Scholar 

  2. B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. Mu noz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual-Version V6.1. Technical Report 0203, INRIA, August 1997.

    Google Scholar 

  3. D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. Refinement in Ergo. Technical report 94-44, Software Verification Research Centre, School of Information Technology, The University of Queensland, Brisbane 4072. Australia, November 1994.

    Google Scholar 

  4. T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76:96–120, 1988.

    Article  MathSciNet  Google Scholar 

  5. E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

    Google Scholar 

  6. J.-C. Filliâtre. Proof of Imperative Programs in Type Theory. In International Workshop, TYPES’ 98, Kloster Irsee, Germany, volume 1657 of Lecture Notes in Computer Science. Springer-Verlag, March 1998.

    Google Scholar 

  7. T. Kleymann. Hoare Logic and VDM: M achine-Checked Soundness and Completeness Proofs. Ph.D. thesis, University of Edinburgh, 1998.

    Google Scholar 

  8. J. Knappmann. A PVS based tool for developing programs in the refinement calculus. Marster’s Thesis, Christian-Albrechts-University, 1996.

    Google Scholar 

  9. L. Laibinis and J. von Wright. Functional procedures in higher-order logic. Technical Report TUCS-TR-252, Turku Centre for Computer Science, Finland, March 15, 1999.

    Google Scholar 

  10. L. Lindqvist. A formalization of Dijkstra’s predicate transformer wp in Martin-Lof type theory. Master’s Thesis, Linkopin University, Sweden, 1997.

    Google Scholar 

  11. Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Number 11 in International Series of Monographs on Computer Science. Oxford University Press, 1994.

    Google Scholar 

  12. C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3):403–419, July 1988.

    Google Scholar 

  13. J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287–306, December 1987.

    Google Scholar 

  14. T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru and V. Vinay, editors, Proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science, pages 180–192. Springer-Verlag LNCS 1180, 1996.

    Google Scholar 

  15. B. Nordström, K. Peterson, and J. M. Smith. Programming in Martin-Lof’s Type Theory, volume 7 of International Series of Monographs on Computer Science. Oxford University Press, New York, NY, 1990.

    Google Scholar 

  16. R. J. R. Back and J. von Wright. Refinement concepts formalized in higher-order logic. Reports on Computer Science & Mathematics Series A—85, Institutionen för Informationsbehandling & Mathematiska Institutet, Åbo Akademi, Lemmink:ainengatan 14, SF-20520 Turku, Finland, September 1989.

    Google Scholar 

  17. M. Staples. A Mechanised Theory of Refinement. Ph.D. Dissertation, Computer Laboratory, University of Cambridge, 1998.

    Google Scholar 

  18. M. Staples. Program transformations and refinements in HOL. In Y. Bertot G. Dowek, C. Paulin, editor, TPHOLs: The 12th International Conference on Theorem Proving in Higher-Order Logics. LNCS, Springer-Verlag., 1999.

    Google Scholar 

  19. J. von Wright and K. Sere. Program transformations and refinements in HOL. In Myla Archer, Jennifer J. Joyce, Karl N. Levitt, and Phillip J. Windley, editors, Proceedigns of the International Workshop on the HOL Theorem Proving System and its Applications, pages 231–241, Los Alamitos, CA, USA, August 1992. IEEE Computer Society Press.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Durham Science Laboratories, South Road, Durhram, DH1 3LE, UK

    Xingyuan Zhang & Malcolm Munro

  2. Department of Information Systems and Computing, Brunel University, Uxbridge, Middlesex, UB8 3PH, UK

    Mark Harman & Lin Hu

Authors
  1. Xingyuan Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Malcolm Munro
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mark Harman
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lin Hu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, MS 130, Hampton, VA, 23681, USA

    Victor A. Carreño

  2. ICASE-Langley Research Center, MS 132C, Hampton, VA, 23681, USA

    César A. Muñoz

  3. Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve Blvd.W., Montréal, Québec, H3G 1M8, Canada

    Sofiène Tahar

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhang, X., Munro, M., Harman, M., Hu, L. (2002). Weakest Precondition for General Recursive Programs Formalized in Coq. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2002. Lecture Notes in Computer Science, vol 2410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45685-6_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-45685-6_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44039-0

  • Online ISBN: 978-3-540-45685-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation