X. Zhang
Weakest precondition for general recursive programs formalized in coq
Zhang, X.; Munro, M.; Harman, M.; Hu, L.
Authors
M. Munro
M. Harman
L. Hu
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.
Citation
Zhang, X., Munro, M., Harman, M., & Hu, L. (2002, January). Weakest precondition for general recursive programs formalized in coq. Presented at 15th International Conference on Theorem Proving in Higher Order Logics : TPHOLs., Hampton, VA
Presentation Conference Type | Conference Paper (Published) |
---|---|
Conference Name | 15th International Conference on Theorem Proving in Higher Order Logics : TPHOLs. |
Publication Date | Aug 23, 2002 |
Deposit Date | Aug 24, 2006 |
Publicly Available Date | Mar 10, 2010 |
Print ISSN | 0302-9743 |
Pages | 332-347 |
Series Title | Lecture notes in computer science |
Series Number | 2410 |
Series ISSN | 0302-9743,1611-3349 |
Book Title | 15th International Conference on Theorem Proving in Higher Order Logics ; proceedings. |
ISBN | 9783540440390 |
DOI | https://doi.org/10.1007/3-540-45685-6_22 |
Keywords | Weakest precondition, Operational semantics, Formal verification. |
Public URL | https://durham-repository.worktribe.com/output/1163568 |
Additional Information | Theorem proving in higher order logics : Proceedings of the 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Vol. 2410. |
Files
Accepted Conference Proceeding
(174 Kb)
PDF
Copyright Statement
The final publication is available at Springer via http://dx.doi.org/10.1007/3-540-45685-6_22
You might also like
CbSSDF and OWL-S, A Scenario based Solution Analysis and Comparison
(2009)
Presentation / Conference Contribution
Pedagogic data as a basis for Web service fault models
(2005)
Presentation / Conference Contribution
An Overview of Regression Testing
(2017)
Journal Article
A Service Scheduling Security Model for a Cloud Environment
(2020)
Journal Article
Evaluating a Cloud Service using Scheduling Security Model (SSM)
(2019)
Journal Article
Downloadable Citations
About Durham Research Online (DRO)
Administrator e-mail: dro.admin@durham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search