zbMATH — the first resource for mathematics

Weakest precondition for general recursive programs formalized in Coq. (English) Zbl 1013.68202
Carreño, Victor A. (ed.) et al., Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2410, 332-347 (2002).
Summary: 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.
For the entire collection see [Zbl 0997.00025].

MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B35 Mechanization of proofs and logical operations
Coq
Full Text: