Weakest Precondition Calculus, Revisited using Why3

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.