4 hoare logic

Hoare logic: formal system to prove program correctness instead of testing.

Hoare Triple: $\{\phi \}C\{\psi \}$ — “If precondition $\phi$ holds and $C$ terminates, then postcondition $\psi$ holds”

2. Validity (45 sec)

Triple	Valid?	Why?
$\{\top \}$ i+=1 $\{\top \}$	✓	True always holds
$\{\perp \}$ i+=1 $\{\perp \}$	✓	Precondition never satisfied → trivially valid
$\{i<n\}$ i+=1 $\{i\le n\}$	✓	$i<n$ then $i+1\le n$ ✓
$\{i<n\}$ i+=1 $\{i<n\}$	✗	Counterexample: $i=1,n=2$

3. Core Rules (1.5 min)

Assignment (read backwards): $\{\psi [e/x]\}$ x := e $\{\psi \}$

• Ex: $\{?\}$ x:=x+1 $\{x>5\}$ → substitute → $\{x>4\}$
• You take the goal and undo the assignment in your head

Sequence: $\frac{\{\phi \}{C}_1\{{\phi }^{\prime }\}\{{\phi }^{\prime }\}{C}_2\{\psi \}}{\{\phi \}{C}_1;C_2\{\psi \}}$

• it is about chaining two statements together by finding an intermediate condition.

While: $\frac{\{\theta \wedge b\}{C}_0\{\theta \}}{\{\theta \}\text{ while }b\text{ do }{C}_0\{\theta \wedge \neg b\}}$ — requires loop invariant $\theta$

“For while loops, we need a loop invariant — a condition that is true before the loop starts, stays true after every iteration, and when the loop ends, combined with the loop being finished, gives us our postcondition.”

4. Loop Invariants (1 min)

Property that holds before and after every iteration: $\{\theta \wedge b\}{C}_0\{\theta \}$

Ex: while (i<n) {i+=1} — Invariant $i\le n$? Check: $\{i<n\wedge i\le n\}$ i+=1 $\{i\le n\}$ ✓

Finding good invariants is the hard part — must be strong enough for postcondition!

5. Properties (15 sec)

• Sound: derivable → valid ✓
• Not complete: some valid triples not derivable (undecidable)
• Relatively complete (Cook ‘74): complete if invariants expressible & side conditions provable

---

All Rules (System H)

Rule	Form
Skip	$\{\phi \}$ skip $\{\phi \}$
Assign	$\{\psi [e/x]\}$ x := e $\{\psi \}$
Seq	$\frac{\{\phi \}{C}_1\{{\phi }^{\prime }\}\{{\phi }^{\prime }\}{C}_2\{\psi \}}{\{\phi \}{C}_1;C_2\{\psi \}}$
Cond	$\frac{\{\phi \wedge b\}{C}_1\{\psi \}\{\phi \wedge \neg b\}{C}_2\{\psi \}}{\{\phi \}\text{ if }b\text{ then }{C}_1\text{ else }{C}_2\{\psi \}}$
While	$\frac{\{\theta \wedge b\}{C}_0\{\theta \}}{\{\theta \}\text{ while }b\text{ do }{C}_0\{\theta \wedge \neg b\}}$
Conseq	$\frac{\{\phi \}C\{\psi \}}{\{{\phi }^{\prime }\}C\{{\psi }^{\prime }\}}$ if ${\phi }^{\prime }\to \phi$ and $\psi \to {\psi }^{\prime }$

Common Invariant Patterns

• Counter bounds: $0\le i\le n$
• Accumulator: $result=f(i)$ where $f$ is partial computation
• Relationship: $x\cdot y=x_0\cdot y_0$ (for multiplication by addition)