Weakest Precondition for General Recursive Programs Formalized in Coq

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.

• Type: Conference
• Year: 2002
• Where: TPHOL
• Authors: Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu
• Keywords: Automated Reasoning, General Recursive Programs, Operational Semantics, Proof Assistant Coq, TPHOL 2002