Hoare Logic (Loops)

Loop Invariant (Partial Correctness)

• Property holds before execution, after each iteration, and after termination.

• Rule {P ∧ B} S {P} ensures invariant is maintained.

• After loop: P ∧ ¬B holds.

While Rule (Partial Correctness)

• {P ∧ B} S {P} implies {P} while B {S} {P ∧ ¬B}.
• Proves loop termination, ensures postcondition holds.
• Does not guarantee termination.

Loop Variant (Total Correctness)

• Integer expression v that decreases with each iteration.
• Must satisfy: P ∧ B → v ≥ 0.
• Proves termination: {P ∧ B ∧ v = V} S {v < V}.

While Rule (Total Correctness)

• Requirements:
  • {P ∧ B} S {P} (invariant preserved).
  • {P ∧ B ∧ v = V} S {v < V} (variant decreases).
  • P ∧ B → v ≥ 0 (variant bounded).
• Concludes {P} while B {S} {P ∧ ¬B}.

Euclid's Algorithm Example

• Computes quotient q and remainder r:
  • r := x; q := 0;
  • while (y ≤ r) { r := r - y; q := 1 + q; }.
• Postcondition: r < y ∧ x = r + y*q.

Euclid Loop Invariant

• Invariant: x = r + y*q.
• Holds initially: x = x + y*0.
• Preserved by iteration: ((r-y) + y(q+1) = r + yq).
• Loop exit r < y gives postcondition.

Euclid Loop Variant

• Variant: r (the remainder).
• Decreases each iteration (r := r - y, with y>0).
• Bounded below by 0, proves termination.

Termination Importance

• Necessary to ensure programs finish.
• Illustrative examples: Zune bug, spinning wheel.
• Total correctness combines partial correctness with termination guarantee.

Compact Proof Representation

• Numbered lines with dependencies:
  • (1) {x>2} x:=x+1 {x>2} CONSEQUENCE
  • (2)(3)(4): (2) x>3→x>2; (3) {x+1>3} x:=x+1 {x>3} ASSIGNMENT; (4) x>2→x+1>3.

Proof Tree Structure

• Root is goal statement.
• Apply rules backward to create sub-goals.
• Leaves closed by axioms (assignment) or implications.
• Shows compact representation with steps, rules, and dependencies.

Sir Tony Hoare (1934-2026)

• Pioneer of Hoare Logic and Quicksort.
• Contributed to CSP (Communicating Sequential Processes) and UTP (Unifying Theories of Programming).
• Passed away March 5, 2026.