Doing a complete proof in Hoare Logic can feel overly verbose. The “core” of a proof consists of the preconditions and postconditions surrounding every command; with those, it’s usually possible to infer the complete shape of the proof tree. Decorating programs is a way to informally write down a Hoare logic proof of correctness. The idea is to insert assertion decorations between every “line” of the program. Using this informal evidence, you can reconstruct the full formal proof.
Informal Rules
We’ll set out a few rules to check whether a decorated program represents a valid proof using local consistency checks. The rules, as you’ll see, are informal reflections of the formal inference rules for Hoare logic.
Skip. For skip, the precondition and postcondition should be the same, like this: Sequence. For sequences, a new assertion appears between the two commands. The two halves and must be (recursively) locally consistent: Assignment. Assignments are locally consistent when the precondition is the same as the post-condition except that it substitutes the assigned expression in for the variable: Conditions. An if is locally consistent when both branches are locally consistent after adding the branch condition to each Loops. A while command should be decorated with a loop invariant: Implication. To capture the CONSEQUENCE rule, you can always write a (valid) implication to connect two commands:
Decorating a Program
These informal rules tell you how to verify whether a decorated program is correct, but they don’t by themselves tell you how to construct those decorations (and thereby a proof). You can do this almost mechanically--except for loop invariants, which still require some creativity to concoct.
Here’s an example program: The first step is to decide what we want to prove about this program. So we write a precondition and postcondition for the whole program. Intuitively, the program adds onto the initial value of the variable , so we’ll assert that: This program is a while command, so the next step is to come up with a loop invariant. We’ll set up the structure first. We need an assertion where we can “connect” the loop’s precondition and postcondition to our overall precondition and postcondition using implications, like this: On every iteration of the loop, the variable is the sum we want, , less the current value of , which is the number of iterations remaining. So we’ll define the invariant like this: The top implication follows because , and the bottom implication is valid because and together imply .
To finish decorating the program, we need an assertion between the two lines in the body of the loop. By the rule for assignments, we know that this must be , or: To make the assignment to locally consistent, then, its precondition must be , or: It’s straightforward to see that the precondition at the top of the loop, implies this new assertion . Now we can write our complete decorated program using these definitions:
