Sciweavers

TPHOL
2002
IEEE

Weakest Precondition for General Recursive Programs Formalized in Coq

13 years 7 months ago
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.
Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu
Added 16 Jul 2010
Updated 16 Jul 2010
Type Conference
Year 2002
Where TPHOL
Authors Xingyuan Zhang, Malcolm Munro, Mark Harman, Lin Hu
Comments (0)