Skip to Main content Skip to Navigation
Reports

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

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-00766171
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

File

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

Identifiers

  • HAL Id : hal-00766171, version 1

Collections

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

441

Files downloads

986