A sharp proof rule for procedures in WP semantics (Q1104730)

We present a proof rule for the procedure call that is sharp; that is, the precondition it defines is the weakest precondition that can be inferred solely from the procedure's specification. Thus the rule enforces exactly the abstraction introduced by the specification. If the procedure has formal parameters (`value' x, `value result' y, `result' z), and is called with corresponding actuals (a,b,c), then our rule gives a precondition for the call of \[ (\exists m\cdot U^{x,y}_{a,b}) \wedge (\forall y,z\cdot (\forall m\cdot U^{x,y}_{a,b\quad} \Rightarrow V\quad x_ a) \Rightarrow E^{b,c}_{y,z}) \] where U and V are the pre- and postcondition of the procedure, and E is the postcondition of the call. We give a simple proof of the soundness and sharpness of our rule, and present an example illustrating the non-sharpness of Gries' proof rule.