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: | (AM) Accepted Manuscript Download PDF (171Kb) |
| Status: | Peer-reviewed |
| Publisher Web site: | http://dx.doi.org/10.1007/3-540-45685-6_22 |
| Publisher statement: | The final publication is available at Springer via http://dx.doi.org/10.1007/3-540-45685-6_22 |
| Date accepted: | No date available |
| Date deposited: | 10 March 2010 |
| Date of first online publication: | January 2002 |
| Date first made open access: | No date available |
Save or Share this output
| Export: | |
| Look up in GoogleScholar |
