Weakest precondition for general recursive programs formalized in coq

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

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, January). Weakest precondition for general recursive programs formalized in coq. Presented at 15th International Conference on Theorem Proving in Higher Order Logics : TPHOLs., Hampton, VA

• Presentation Conference Type: Conference Paper (published)
• Conference Name: 15th International Conference on Theorem Proving in Higher Order Logics : TPHOLs.
• Publication Date: Aug 23, 2002
• Deposit Date: Aug 24, 2006
• Publicly Available Date: Mar 10, 2010
• Print ISSN: 0302-9743
• 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.
• Public URL: https://durham-repository.worktribe.com/output/1163568
• 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.