Skip to Main content Skip to Navigation

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 :
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Claude Marché <>
Submitted on : Monday, December 17, 2012 - 5:10:54 PM
Last modification on : Thursday, July 8, 2021 - 3:49:23 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