Cookies

We use cookies to ensure that we give you the best experience on our website. You can change your cookie settings at any time. Otherwise, we'll assume you're OK to continue.

Durham University

Computer Science

Profile

Publication details for Professor Malcolm Munro

Zhang, X. , Munro, M. , Harman, M. & Hu, L. (2002), Weakest precondition for general recursive programs formalized in coq, Lecture notes in computer science 2410: 15th International Conference on Theorem Proving in Higher Order Logics TPHOLs. Hampton, VA., Springer, Hampton VA, 332-347.
  • Publication type: Conference Paper
  • ISSN/ISBN: 0302-9743
  • Keywords: Weakest precondition, Operational semantics, Formal verification.
  • Durham Research Online (DRO) - may include full text

Author(s) from Durham

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.

References

1. R. J. R. Back. A calculus of re nements for program derivations. Acta Informatica,
25(6):593{624, August 1988.
2. B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Gimenez, H. Herbelin,
G. Huet, C. Mu noz, C. Murthy, C. Parent, C. Paulin, A. Sabi, and B. Werner.
The Coq Proof Assistant Reference Manual { Version V6.1. Technical Report 0203,
INRIA, August 1997.
3. D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. Re nement in
Ergo. Technical report 94-44, Software Veri cation Research Centre, School of
Information Technology, The University of Queensland, Brisbane 4072. Australia,
November 1994.
4. T. Coquand and G. Huet. The Calculus of Constructions. Information and Com-
putation, 76:96{120, 1988.
5. E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
6. J.-C. Filli^atre. 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.
7. T. Kleymann. Hoare Logic and VDM: Machine-Checked Soundness and Complete-
ness Proofs. Ph.D. thesis, University of Edinburgh, 1998.
8. J. Knappmann. A PVS based tool for developing programs in the re nement cal-
culus. Marster's Thesis, Christian-Albrechts-University, 1996.
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.
10. L. Lindqvist. A formalization of Dijkstra's predicate transformer wp in Martin-Lof
type theory. Master's Thesis, Linkopin University, Sweden, 1997.
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.
12. C. Morgan. The speci cation statement. ACM Transactions on Programming
Languages and Systems, 10(3):403{419, July 1988.
13. J. M. Morris. A theoretical basis for stepwise re nement and the programming
calculus. Science of Computer Programming, 9(3):287{306, December 1987.
14. T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook.
In V. Chandru and V. Vinay, editors, Proceedings of the Conference on Founda-
tions of Software Technology and Theoretical Computer Science, pages 180{192.
Springer-Verlag LNCS 1180, 1996.
15. B. Nordstrom, 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.
16. R. J. R. Back and J. von Wright. Re nement concepts formalized in higherorder
logic. Reports on Computer Science & Mathematics Series A|85, Institutionen
for Informationsbehandling & Mathematiska Institutet, Abo Akademi,
Lemminkainengatan 14, SF-20520 Turku, Finland, September 1989.
17. M. Staples. A Mechanised Theory of Re nement. Ph.D. Dissertation, Computer
Laboratory, University of Cambridge, 1998.
18. M. Staples. Program transformations and re nements in HOL. In Y. Bertot
G. Dowek, C. Paulin, editor, TPHOLs: The 12th International Conference on The-
orem Proving in Higher-Order Logics. LNCS, Springer-Verlag., 1999.
19. J. von Wright and K. Sere. Program transformations and re nements 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.

Notes

Theorem proving in higher order logics : Proceedings of the 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002.
Vol. 2410.