Decorated Programs

The beauty of Hoare Logic is that it is compositional: the structure of proofs exactly follows the structure of programs. This suggests that we can record the essential ideas of a proof (informally, and leaving out some low-level calculational details) by "decorating" a program with appropriate assertions on each of its commands. Such a decorated program carries within it an argument for its own correctness.

For example, consider the program: (Note the parameters m and p, which stand for fixed-but-arbitrary numbers. Formally, they are simply Coq variables of type nat.)

Here is one possible specification for this program:

Here is a decorated version of the program, embodying a proof of this specification: Concretely, a decorated program consists of the program text interleaved with assertions (either a single assertion or possibly two assertions separated by an implication).

To check that a decorated program represents a valid proof, we check that each individual command is locally consistent with its nearby assertions in the following sense:

• SKIP is locally consistent if its precondition and postcondition are the same:
         {{ P }} SKIP {{ P }}

• The sequential composition of c₁ and c₂ is locally consistent (with respect to assertions P and R) if c₁ is locally consistent (with respect to P and Q) and c₂ is locally consistent (with respect to Q and R):
         {{ P }} c₁;; {{ Q }} c₂ {{ R }}

• An assignment is locally consistent if its precondition is the appropriate substitution of its postcondition:
         {{ P [X |-> a] }}
         X ::= a
         {{ P }}

• A conditional is locally consistent (with respect to assertions P and Q) if the assertions at the top of its "then" and "else" branches are exactly P ∧ b and P ∧ ¬b and if its "then" branch is locally consistent (with respect to P ∧ b and Q) and its "else" branch is locally consistent (with respect to P ∧ ¬b and Q):
         {{ P }}
         IFB b THEN
           {{ P ∧ b }}
           c₁
           {{ Q }}
         ELSE
           {{ P ∧ ¬b }}
           c₂
           {{ Q }}
         FI
         {{ Q }}

• A while loop with precondition P is locally consistent if its postcondition is P ∧ ¬b, if the pre- and postconditions of its body are exactly P ∧ b and P, and if its body is locally consistent:
         {{ P }}
         WHILE b DO
           {{ P ∧ b }}
           c₁
           {{ P }}
         END
         {{ P ∧ ¬b }}

• A pair of assertions separated by ->> is locally consistent if the first implies the second:
         {{ P }} ->>
         {{ P' }}
  This corresponds to the application of hoare_consequence, and it is the only place in a decorated program where checking whether decorations are correct is not fully mechanical and syntactic, but rather may involve logical and/or arithmetic reasoning.

Example: Swapping Using Addition and Subtraction

Here is a program that swaps the values of two variables using addition and subtraction (instead of by assigning to a temporary variable). We can prove using decorations that this program is correct — i.e., it always swaps the values of variables X and Y.

Example: Simple Conditionals

Here's a simple program using conditionals, with a possible specification: Let's turn it into a decorated program...

Example: Division

The following Imp program calculates the integer quotient and remainder of two numbers m and n that are arbitrary constants in the program. In we replace m and n by concrete numbers and execute the program, it will terminate with the variable X set to the remainder when m is divided by n and Y set to the quotient.

Here's a possible specification:

Finding Loop Invariants

Once the outer pre- and postcondition are chosen, the only creative part in verifying programs using Hoare Logic is finding the right loop invariants...

Example: Slow Subtraction

The following program subtracts the value of X from the value of Y by repeatedly decrementing both X and Y. We want to verify its correctness with respect to the pre- and postconditions shown:

To verify this program, we need to find an invariant I for the loop. As a first step we can leave I as an unknown and build a skeleton for the proof by applying the rules for local consistency (working from the end of the program to the beginning, as usual, and without any thinking at all yet). This leads to the following skeleton: By examining this skeleton, we can see that any valid I will have to respect three conditions:

• (a) it must be weak enough to be implied by the loop's precondition, i.e., (1) must imply (2);
• (b) it must be strong enough to imply the program's postcondition, i.e., (7) must imply (8);
• (c) it must be preserved by one iteration of the loop, i.e., (3) must imply (4).

Example: Parity

Here is a cute little program for computing the parity of the value initially stored in X (due to Daniel Cristofani). The mathematical parity function used in the specification is defined in Coq as follows:

Example: Finding Square Roots

The following program computes the (integer) square root of X by naive iteration:

Example: Squaring

Here is a program that squares X by repeated addition:

Formal Decorated Programs (Optional)

With a little more work, we can formalize the definition of well-formed decorated programs and mostly automate the mechanical steps when filling in decorations...

Syntax

The first thing we need to do is to formalize a variant of the syntax of commands with embedded assertions. We call the new commands decorated commands, or dcoms. We don't want both preconditions and postconditions on each command, because a sequence of two commands would contain redundant decorations, the postcondition of the first likely being the same as the precondition of the second. Instead, decorations are added corresponding to each postcondition. A separate type, decorated, is used to add the precondition for the entire program.

Here's how our decorated programs look now:

It is easy to go from a dcom to a com by erasing all annotations.

The choice of exactly where to put assertions in the definition of dcom is a bit subtle. The simplest thing to do would be to annotate every dcom with a precondition and postcondition. But this would result in very verbose programs with a lot of repeated annotations: for example, a program like SKIP;SKIP would have to be annotated as with pre- and post-conditions on each SKIP, plus identical pre- and post-conditions on the semicolon! Instead, the rule we've followed is this:

• The post-condition expected by each dcom d is embedded in d.
• The pre-condition is supplied by the context.

In other words, the invariant of the representation is that a dcom d together with a precondition P determines a Hoare triple {{P}} (extract d) {{post d}}, where post is defined as follows:

It is straightforward to extract the precondition and postcondition from a decorated program.

We can express what it means for a decorated program to be correct as follows:

To check whether this Hoare triple is valid, we need a way to extract the "proof obligations" from a decorated program. These obligations are often called verification conditions.

Extracting Verification Conditions

The function verification_conditions takes a dcom d together with a precondition P and returns a proposition that, if it can be proved, implies that the triple {{P}} (extract d) {{post d}} is valid.

And now the key theorem, stating that verification_conditions does its job correctly. Not surprisingly, we need to use each of the Hoare Logic rules at some point in the proof.

Automation

Now that all the pieces are in place, we can verify an entire program.

The propositions generated by verification_conditions are fairly big, and they contain many conjuncts that are essentially trivial.

In principle, we could work with such propositions using just the tactics we have so far, but we can make things much smoother with a bit of automation. We first define a custom verify tactic that uses split repeatedly to turn all the conjunctions into separate subgoals and then uses omega and eauto (described in chapter Auto in Logical Foundations) to deal with as many of them as possible.

What's left after verify does its thing is "just the interesting parts" of checking that the decorations are correct. For very simple examples verify immediately solves the goal (provided that the annotations are correct!).

Another example (formalizing a decorated program we've seen before):

Examples

In this section, we use the automation developed above to verify formal decorated programs corresponding to most of the informal ones we have seen.

Swapping Using Addition and Subtraction

Simple Conditionals

See the full version of the chapter for the rest...