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).
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)
|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|
|Record Created:||24 Aug 2006|
|Last Modified:||31 Mar 2015 13:07|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Look up in GoogleScholar | Find in a UK Library|