L08 - Hoare Proof System

Back to Program Verification Index | Previous: (y-07) Relational Semantics | Next: (y-09) Ultimate Referee

Mental Model for the Hoare Proof System

• Semantics says what a program does. Relational semantics gives the exact before/after relation of a statement.
• Hoare logic gives a proof method. Instead of calculating the whole relation, prove local triples and compose them.
• The proof object is a tree. Every node is a Hoare triple; every edge is justified by one rule and any required side condition.
• Loops need insight. The while rule is mechanical once an inductive invariant is chosen, but finding that invariant is the hard part.

---

1. Hoare Triples and Validity

A Hoare triple has the form:

$\{\phi \}st\{\psi \}$

• $\phi$: precondition, a set of allowed starting states.
• $st$: the Boostan statement.
• $\psi$: postcondition, the set of accepted final states.

The triple is valid iff st satisfies the precondition-postcondition pair:

$post(\{\phi \},[[st]])\subseteq \{\psi \}$

So validity is still semantic; the proof system is just a structured way to establish it.

Proof Systems Compared

The course has already used proof systems for formulas:

• NPL derives valid propositional implications.
• NFOL derives valid first-order implications.
• Hoare proof system derives valid program triples.

The shape is analogous: syntax-driven rules produce objects that are guaranteed to be semantically valid if the system is sound.

---

2. Rules of the Hoare Proof System

The core rules are:

1. Assignment axiom: reason backward through x := expr.
2. Composition rule: split st1; st2 using an intermediate assertion.
3. Strengthen precondition: replace a precondition by a stronger one.
4. Weaken postcondition: replace a postcondition by a weaker one.
5. Conditional rule: prove both branches under the appropriate guard.
6. While rule: prove the body preserves an invariant.

Derivations as Trees

A derivation is a tree whose labels are Hoare triples. For a parent node to be legal, its children must match one of the proof rules. This is important because a derivation is checkable: once the formulas and invariants are written down, the proof rules decide whether the tree is valid.

Assignment and Composition

The assignment axiom is:

$\{\phi [x\mapsto expr]\}x:=expr;\{\phi \}$

Read it backward: to make $\phi$ true after assignment, require $\phi$ with x replaced by expr before assignment.

The composition rule is:

$$\frac{\{{\phi }_1\}s{t}_1\{{\phi }_2\}\{{\phi }_2\}s{t}_2\{{\phi }_3\}}{\{{\phi }_1\}s{t}_{1}s{t}_2\{{\phi }_3\}}$$

The intermediate assertion ${\phi }_2$ is the contract between the two statements.

---

3. Branches and Loops

Conditional Rule

For if (expr) { st1 } else { st2 }, prove:

$\{\phi \wedge expr\}s{t}_1\{\psi \}$

and

$\{\phi \wedge \neg expr\}s{t}_2\{\psi \}$

Both branches must establish the same postcondition. The guard only decides which branch relation is active.

While Rule and Invariants

The while rule is:

$$\frac{\{\phi \wedge expr\}st\{\phi \}}{\{\phi \}while(expr)\{st\}\{\phi \wedge \neg expr\}}$$

The formula $\phi$ is an inductive loop invariant:

• true before the loop,
• preserved by one loop iteration,
• still true when the loop exits.

Hoare Proof System Example

The Pab example shows the typical workflow: choose a loop invariant, push obligations backward through assignments and conditionals, and use consequence rules when the exact syntactic preconditions do not line up.

---

4. Soundness of Individual Rules

Soundness means every derivable triple is actually valid in the relational semantics. The proof strategy is local first: prove that every rule preserves validity.

Assignment Axiom

Assignment is sound because x := expr updates only x. Substituting expr for x in the precondition exactly predicts the formula that must hold after the update.

Composition Rule

Composition is sound because postimages compose. If st1 reaches only ${\phi }_2$ states, and st2 reaches only ${\phi }_3$ states from there, then st1; st2 reaches only ${\phi }_3$ states.

Consequence Rules

Strengthening the precondition is safe because it reduces the set of starting states.

Weakening the postcondition is safe because it enlarges the set of accepted final states.

---

5. Soundness of Control Flow

Conditional Rule

The conditional relation is the union of two guarded branch relations. If the then branch is valid under expr and the else branch is valid under !expr, the whole conditional is valid.

While Rule

The loop semantics uses reflexive transitive closure. The proof shows by induction over the number of iterations that the invariant is preserved after every finite loop execution. At exit, the guard is false, so the postcondition is $\phi \wedge \neg expr$.

---

6. Soundness of the Whole System

The final theorem is:

If there is a derivation whose root is labelled by $\{\phi \}st\{\psi \}$, then st satisfies the precondition-postcondition pair $(\{\phi \},\{\psi \})$.

The proof is by induction over derivation height:

1. Leaves are justified by sound axioms.
2. Children of an internal node are valid by the induction hypothesis.
3. The applied proof rule preserves validity.
4. Therefore the root triple is valid.

---

Summary

• A Hoare triple connects a precondition, a statement, and a postcondition.
• The proof system derives triples using local syntactic rules.
• Assignment works backward through substitution.
• Composition needs an intermediate assertion.
• Conditionals split by the guard.
• Loops require an inductive invariant.
• Soundness bridges derivability back to relational semantics.

Self-Check

1. State the validity condition for a Hoare triple $\{\phi \}st\{\psi \}$ in semantic terms.

Answer

The triple is valid iff $\text{post}(\{\phi \},[[st]])\subseteq \{\psi \}$: every final state reachable from a $\phi$-state through $st$ lies in $\psi$. The proof system is just a structured way to establish that semantic inclusion.

2. Write the assignment axiom and explain why it reads “backward”.

Answer

$\{\phi [x\mapsto expr]\}x:=expr\{\phi \}$. To make $\phi$ true after the assignment, the state before must satisfy $\phi$ with every free occurrence of $x$ replaced by $expr$. The rule pushes the postcondition through the assignment back into a precondition, which is why proofs are typically done from the end backward.

3. Why does the composition rule need an intermediate assertion ${\phi }_2$?

Answer

The composition rule says $\{{\phi }_1\}s{t}_1\{{\phi }_2\}$ and $\{{\phi }_2\}s{t}_2\{{\phi }_3\}$ together give $\{{\phi }_1\}s{t}_1;s{t}_2\{{\phi }_3\}$. The intermediate ${\phi }_2$ is the contract between the two pieces: it must be implied by what $s{t}_1$ guarantees and strong enough for $s{t}_2$ to need. Picking a good ${\phi }_2$ is the main creative step in sequential proofs.

4. State the three requirements for $\phi$ to be a loop invariant in the while rule.

Answer

$\phi$ must hold before the loop (so it implies the loop’s precondition), be preserved by one iteration assuming the guard holds (i.e., $\{\phi \wedge expr\}st\{\phi \}$ is derivable), and combine with $\neg expr$ on exit to imply the desired postcondition. The rule yields $\{\phi \}\text{while}(expr)\{st\}\{\phi \wedge \neg expr\}$.

5. What does soundness of the Hoare proof system mean, and how is the soundness theorem proved?

Answer

Soundness means every derivable triple is actually valid in the relational semantics. The proof is by induction on the height of the derivation: leaves are justified by sound axioms (assignment, plus side conditions), the induction hypothesis gives validity of all immediate sub-derivations, and each proof rule is shown locally to preserve validity. Combining these gives validity at the root.

---

Back to Program Verification Index | Previous: (y-07) Relational Semantics | Next: (y-09) Ultimate Referee | (y) Return to Notes | (y) Return to Home