Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Weakest Precondition Calculus, Revisited using Why3

Claude Marché 1, 2 Asma Tafat 1 
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : This report has two objectives. First, we present an original method of proof of soundness of a weakest precondition calculus, based on the notion of blocking semantics. The method mimics, at the level of logic specifications, the classical proof of type soundness. Moreover, the proof is performed formally using the Why3 environment for deductive verification, and we illustrate, along the development of the case study, the advanced features of Why3 we used. The result is a revisited presentation the weakest precondition calculus which is easy to follow, although formally made, thanks in particular to the high degree of proof automation that allows us to focus on the key points.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-00766171
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Monday, December 17, 2012 - 5:10:54 PM
Last modification on : Friday, October 28, 2022 - 3:28:38 AM
Long-term archiving on: : Sunday, December 18, 2016 - 3:52:13 AM

File

RR-8185.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00766171, version 1

Citation

Claude Marché, Asma Tafat. Weakest Precondition Calculus, Revisited using Why3. [Research Report] RR-8185, INRIA. 2012, pp.32. ⟨hal-00766171⟩

Share

Metrics

Record views

202

Files downloads

834