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\}$

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

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

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 }$

Factorial Example

{n ≥ 0}  f := 1; i := 1;
while i ≤ n do ⟨f = fact(i-1) ∧ 1 ≤ i ≤ n+1⟩
  { f := f·i; i := i+1 }
{f = fact(n)}

Key Definitions

• Valid: $\forall s,s^{\prime }$: if $[[\phi ]](s)=T$ and $(C,s)⇝s^{\prime }$ then $[[\psi ]](s^{\prime })=T$
• Auxiliary vars: in $\phi$/$\psi$ but not in $C$ (e.g., $x_0$ for initial value)
• Loop unfolding: while $b$ do $C$ $\equiv$ if $b$ then $(C;$ while $b$ do $C)$ else skip

Proof Strategy

1. Work bottom-up from conclusion
2. Assignments: substitute backwards into postcondition
3. While: identify invariant $\theta$, show $\{\theta \wedge b\}{C}_0\{\theta \}$, conclude $\{\theta \}$while$\{\theta \wedge \neg b\}$
4. Use consequence rule to bridge logical gaps
5. Verify side conditions (${\phi }^{\prime }\to \phi$, $\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)