Weakest precondition

Summary

The weakest precondition $\mathrm{wp}(C, Q)$ of a command $C$ and a postcondition $Q$ is a condition on the starting state. It is the most general condition that guarantees that $C$ terminates in a state satisfying $Q$. Edsger W. Dijkstra introduced it in 1975, with his language of guarded commands. He used it to define the meaning of programs and to derive programs from their specifications. The map $Q \mapsto \mathrm{wp}(C, Q)$ is a predicate transformer, and it can be computed by structural rules for every construct except loops. It is the backward-reasoning counterpart of Hoare logic and the basis of many verification tools.