Hoare Logic (Sequential and Conditionals)

Inference Rule Structure

• A₁, A₂, …, Aₙ / C: Valid antecedents lead to valid consequence C.

• Axiom: Inference rule without antecedents.

• Used in proof trees: root = statement to prove, leaves = axioms.

Hoare Logic Proof Procedure

• Start with statement as root.
• Choose rule to break it down into sub-goals.
• Apply rules backward until all leaves are closed.

Rule of Composition

• {P} S {R}, {R} T {Q} => {P} S; T {Q}.
• Requires intermediate assertion R linking S's postcondition to T's precondition.
• Generalized for multiple statements.

Composition Precondition Calculation

• Compute intermediate assertions by backward substitution.
• Work backwards from postcondition, applying substitutions for each assignment.

Rule of Conditional

• {P ∧ G} S {Q}, {P ∧ ¬G} T {Q} => {P} if G {S} {T} {Q}.
• G branches: True -> S executes; False -> T executes.

Conditional Proof Example

• Prove: {x ≠ 0} if (x < 0) {x := -x} {x := x} {x > 0}.
• Cases: x

Backward Reasoning Approach

• Proofs built backward: start from postcondition, work toward precondition.
• Substitute backward for assignments.
• Split cases for conditionals.

Proof Tree Construction

• Root: statement to prove.
• Decompose into sub-goals with chosen rules.
• Valid when all branches are proven.

Intermediate Assertion Role

• R must be strong enough to follow from S's execution.
• Weak enough to imply T's precondition.
• Found by back-calculating from final postcondition.