5 Weakest precondition

Definition
$wp(C,\psi )$ = the most general condition that, if true before $C$, guarantees $\psi$ afterwards.

Core equivalence
$\{\phi \}C\{\psi \}$ is valid $⟺\phi \to wp(C,\psi )$

---

Backward rules (compute inside-out)

construct	rule
skip	$wp(\text{skip},\psi )=\psi$
assignment	$wp(x:=e,\psi )=\psi [e/x]$
sequence	$wp(C_1;C_2,\psi )=wp(C_1,wp(C_2,\psi ))$
conditional	$wp(\text{if }b\text{ then }{C}_1\text{ else }{C}_2,\psi )=(b\to wp(C_1,\psi ))\wedge (\neg b\to wp(C_2,\psi ))$
while	needs user-given invariant $\theta$; check $\phi \to \theta$, $\{\theta \wedge b\}C\{\theta \}$, $\theta \wedge \neg b\to \psi$

---

Live example (same one every time)

Program: x:=x+1; y:=x*2
Post: $y=12$

1. $wp(y:=x\ast 2,y=12)=x\ast 2=12=x=6$
2. $wp(x:=x+1,x=6)=x+1=6=x=5$

Hence $\{x=5\}$ code $\{y=12\}$ ✓

Any other precondition stronger than $x=5$ also works; $x=5$ is the weakest.