Cookies

We use cookies to ensure that we give you the best experience on our website. You can change your cookie settings at any time. Otherwise, we'll assume you're OK to continue.


Durham Research Online
You are in:

Weakest precondition for general recursive programs formalized in Coq.

Zhang, X. and Munro, M. and Harman, M. and Hu, L. (2002) 'Weakest precondition for general recursive programs formalized in Coq.', in 15th International Conference on Theorem Proving in Higher Order Logics ; proceedings. Berlin: Springer, pp. 332-347. Lecture notes in computer science. (2410).

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.

Item Type:Book chapter
Additional Information:Conference held on August 20-23, 2002, Hampton, VA, USA.
Keywords:Weakest precondition, Operational semantics, Formal verification.
Full text:PDF (Copyright agreement prohibits open access to the full-text) - Accepted Version
Publisher-imposed embargo
(171Kb)
Status:Peer-reviewed
Publisher Web site:http://dx.doi.org/10.1007/3-540-45685-6_22
Record Created:24 Aug 2006
Last Modified:09 Oct 2014 13:36

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Usage statisticsLook up in GoogleScholar | Find in a UK Library