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
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


Files produced by the author(s)


  • HAL Id : hal-00766171, version 1


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



Record views


Files downloads