Skip to main content

Research Repository

Advanced Search

Weakest precondition for general recursive programs formalized in coq

Zhang, X.; Munro, M.; Harman, M.; Hu, L.

Weakest precondition for general recursive programs formalized in coq Thumbnail


Authors

X. Zhang

M. Munro

M. Harman

L. Hu



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.

Citation

Zhang, X., Munro, M., Harman, M., & Hu, L. (2002). Weakest precondition for general recursive programs formalized in coq. In 15th International Conference on Theorem Proving in Higher Order Logics ; proceedings (332-347). https://doi.org/10.1007/3-540-45685-6_22

Conference Name 15th International Conference on Theorem Proving in Higher Order Logics : TPHOLs.
Conference Location Hampton, VA.
Publication Date Aug 23, 2002
Deposit Date Aug 24, 2006
Publicly Available Date Mar 29, 2024
Pages 332-347
Series Title Lecture notes in computer science
Series Number 2410
Series ISSN 0302-9743,1611-3349
Book Title 15th International Conference on Theorem Proving in Higher Order Logics ; proceedings.
ISBN 9783540440390
DOI https://doi.org/10.1007/3-540-45685-6_22
Keywords Weakest precondition, Operational semantics, Formal verification.
Additional Information Theorem proving in higher order logics : Proceedings of the 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Vol. 2410.

Files




You might also like



Downloadable Citations