Questions: Hoare Logic

Question 1

What does the Hoare triple {x > 0} x := x - 1 {x >= 0} assert?

• A. If x > 0 before execution and x := x - 1 terminates, then x >= 0 afterward
• B. The program x := x - 1 always terminates with x >= 0
• C. If x >= 0 before execution, then x > 0 afterward
• D. The assignment x := x - 1 is only valid when x > 0

Answer: (A)

A Hoare triple {P} C {Q} is a partial correctness assertion: it says that IF the precondition P holds before executing C, and IF C terminates, THEN the postcondition Q holds afterward. It does not guarantee termination (that would be total correctness), nor does it constrain when the command may be executed.

Question 2

Hoare logic's rule for assignment is {Q[x/E]} x := E {Q}, where Q[x/E] substitutes E for x in Q. This rule works backward from the postcondition, not forward from the precondition.

• T. True
• F. False

Answer: True

The assignment axiom is one of the most counterintuitive aspects of Hoare logic for newcomers. To prove that Q holds after x := E, you must show that Q with E substituted for x held before the assignment. For example, to prove {?} x := x + 1 {x > 5}, substitute x + 1 for x in the postcondition to get the precondition x + 1 > 5, i.e., x > 4. The rule works backward because the assignment determines what must have been true before in order for the postcondition to hold after.

Question 3

What is the difference between partial correctness and total correctness in Hoare logic, and which does the standard Hoare triple {P} C {Q} assert?

Model answer: Partial correctness (standard {P} C {Q}) asserts that IF the program terminates, the postcondition holds. Total correctness ([P] C [Q]) asserts that the program DOES terminate and the postcondition holds. Proving total correctness additionally requires showing termination, typically via a well-founded variant (ranking function) that decreases on each loop iteration.

The distinction matters because a non-terminating program trivially satisfies any partial correctness specification — {true} while(true) skip {false} is valid in partial correctness since the program never terminates, so the postcondition is never checked. Total correctness adds the obligation to prove termination, usually by exhibiting a natural-number-valued expression that strictly decreases with each iteration and cannot decrease forever.

Question 4

In Hoare logic, the rule of consequence allows strengthening the precondition and weakening the postcondition. Why is this sound?

Model answer: If {P} C {Q} holds and P' implies P (stronger precondition) and Q implies Q' (weaker postcondition), then {P'} C {Q'} holds because: starting from a stronger assumption still guarantees P, so Q holds after execution, and since Q implies Q', Q' holds too. The rule lets you adapt proven triples to fit into larger proof contexts.

The rule of consequence is the 'glue' that makes compositional proofs possible. Without it, you would need each subproof to produce exactly the precondition/postcondition needed by adjacent proof steps. With it, you can prove a triple with natural pre/postconditions and then adjust them to interface with surrounding code.