5 Weakest precondition

Problem: Given program $C$ and desired result $\psi$, what must be true before we run it?

Answer: Work backwards—“undo” each statement from the postcondition.

The function: $wp(C,\psi )$ = weakest precondition guaranteeing $\psi$ after $C$

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

---

2. The Five Rules

Rule	Formula	How to say it
skip	$wp(\text{skip},\psi )=\psi$	Does nothing → requirement unchanged
assignment	$wp(x:=e,\psi )=\psi [e/x]$	You take the goal and undo the assignment in your head
sequence	$wp(C_1;C_2,\psi )=wp(C_1,wp(C_2,\psi ))$	it is about chaining two statements together by finding an intermediate condition.
if-else	$(b\to wp(C_1,\psi ))\wedge (\neg b\to wp(C_2,\psi ))$	Both branches must reach the goal
while	needs invariant $\theta$	Can’t compute automatically

Assignment example: Goal $x>5$, statement x := x+1
→ Replace $x$ with $x+1$: $(x+1)>5$ → $x>4$

---

3. Worked Example

Verify: $\{x=5\}$ x := x+1; y := x*2 $\{y=12\}$

Step	Action	Result
Start	Postcondition	$y=12$
1	Undo y := x*2: replace $y$ with $x\ast 2$	$x=6$
2	Undo x := x+1: replace $x$ with $x+1$	$x=5$

Check: $x=5\to x=5$? ✓ Valid.

---

4. Loops (the tricky part) Do not make an example

Loops need a human-supplied invariant $\theta$ (undecidable in general).

Three conditions to verify:

Condition	Formula	Meaning
Initiation	$\phi \to \theta$	Invariant holds at start
Preservation	$\{\theta \wedge b\}{C}_{\text{body}}\{\theta \}$	Loop body maintains it
Exit	$\theta \wedge \neg b\to \psi$	Exiting gives postcondition

---

5. Summary

What	$wp(C,\psi )$ = weakest condition before $C$ to guarantee $\psi$ after
How	Substitute backwards through each statement
Theorem	$\{\phi \}C\{\psi \}$ valid iff $\phi \to wp(C,\psi )$
Loops	Need invariant; verify 3 conditions
Benefit	Automates Hoare logic for loop-free code

---

Quick answers:

• “Weakest” = accepts the most starting states; any stronger precondition also works
• “w.r.t.” = “with respect to”