Hoare Logic and Proving a Program Meets Its Specification
A partial-correctness Hoare triple promises that execution starting in its precondition satisfies its postcondition if it terminates. Rules compose compatible triples. Loop invariants support initialization, preservation and exit checks; termination needs an additional argument. Tools can generate verification conditions, and some can infer invariants.
What a learner can do afterwards
- Prove a short assignment sequence by composing triples with compatible intermediate assertions
- Supply a loop invariant, check initialization and preservation, and derive the postcondition at exit
- Compute an assignment's weakest precondition and distinguish partial correctness from termination
1 · Read
You have checked executions against a specification. Hoare logic reasons symbolically about code. Write {P} C {Q}: precondition P, code C, postcondition Q. Partial correctness promises Q if execution starts in P and terminates. It does not promise termination. Here variables are mathematical integers without overflow, and := means assignment.
For x := x + 2; y := 2*x, start with x = 3. The first line gives x = 5. That assertion supports the second line, which gives y = 10. To compose {P} C1 {R} and {S} C2 {Q}, R must imply S. Two valid triples cannot be joined using intermediate assertions that fail this implication.
Let n be a fixed nonnegative integer. Run i := 0; while i < n do i := i + 1. Invariant 0 <= i <= n holds initially. Under the guard i < n, integer increment preserves both bounds. At exit the false guard gives i >= n; with i <= n, this yields i = n. Check initialization, preservation under the guard, and the exit implication. A stronger invariant needs all three checks again.
Some tools infer invariants; others need annotations from you. A verification-condition generator turns proof obligations into formulas for a solver. The obligations must be valid. A solver result of unknown leaves an obligation unproved: it establishes neither correctness nor a program bug.
For an assignment that terminates, its weakest precondition is the least restrictive starting condition guaranteeing the chosen postcondition. Substitute the assigned expression for the variable in that postcondition. For x := x + 2 and goal x >= 7, obtain x + 2 >= 7, or x >= 5. This works backward from the goal. Forward reasoning is also valid.
Total correctness adds termination. In the counting loop, n - i is a nonnegative integer at each successful guard check and decreases on every iteration, so the loop cannot repeat forever. Invariant checks alone do not give this argument. The loop while true do skip preserves invariant true but never terminates; skip leaves the state unchanged.
Compose compatible triples. Check invariants at entry, through guarded steps and at exit. Total correctness also needs a termination argument.
Original lesson, questions and flashcards about Hoare logic, written for this dataset.
2 · Watch
به انگلیسیTake it off screen
Where it sits
Learn first
This opens up
8 questions wait behind this lesson, each with its answer explained. Every answer feeds the sky: stars light as they are learned, and dim when it is time to come back.