Weakening Rule

(Precondition strengthening, postcondition weakening)

Suppose $\langle \alpha \rangle \; P \; \langle \beta \rangle$ is partially correct. Suppose $\alpha_1 \to \alpha$ is True (if $\alpha_1$ evaluates to True at $x$, so does $\alpha$), and suppose $\beta \to \beta$ is True . So $\alpha_1$ is stronger (or as strong as) $\alpha$, and $\beta$ is stronger than (or as strong as) $\beta_1$. Then also $\langle \alpha_1 \rangle \; P \; \langle \beta_1 \rangle$ is partially correct.

Proof. Suppose $\langle \alpha \rangle \; P \; \langle \beta \rangle$ is partially correct and $\alpha_1 \to \alpha$ and $\beta \to \beta_1$ are both tautologies. Suppose input $x$ satisfies $\alpha_1$. Then $x$ satisfies $\alpha$. So when the code $P$ is applied to $x$, any output satisfies $\beta$ (since $\langle \alpha \rangle \; P \; \langle \beta \rangle$ is partially correct). So any such output satisfies $\beta_1$ (since $\beta \to \beta_1$ is a tautology). So by definition $\langle \alpha \rangle \; P \; \langle \beta_1 \rangle$ is partially corect. $\qedsymbol$