Decorated Programs

The beauty of Hoare Logic is that it is structure-guided: the structure of proofs exactly follows the structure of programs. We can record the essential ideas of a Hoare-logic proof -- omitting low-level calculational details -- by "decorating" a program with appropriate assertions on each of its commands. Such a decorated program carries within itself an argument for its own correctness.

For example, consider the program:
    X := m;
    Z := p;
    while X ≠ 0 do
      Z := Z - 1;
      X := X - 1
    end

Here is one possible specification for this program, in the form of a Hoare triple:
    {{ True }}
    X := m;
    Z := p;
    while X ≠ 0 do
      Z := Z - 1;
      X := X - 1
    end
    {{ Z = p - m }}

Here is a decorated version of this program, embodying a proof of this specification:
    {{ True }} ->>
    {{ m = m }}
      X := m
                         {{ X = m }} ->>
                         {{ X = m ∧ p = p }};
      Z := p;
                         {{ X = m ∧ Z = p }} ->>
                         {{ Z - X = p - m }}
      while X ≠ 0 do
                         {{ Z - X = p - m ∧ X ≠ 0 }} ->>
                         {{ (Z - 1) - (X - 1) = p - m }}
        Z := Z - 1
                         {{ Z - (X - 1) = p - m }};
        X := X - 1
                         {{ Z - X = p - m }}
      end
    {{ Z - X = p - m ∧ ¬(X ≠ 0) }} ->>
    {{ Z = p - m }} Concretely, a decorated program consists of the program's text interleaved with assertions (sometimes multiple assertions separated by implications).

A decorated program can be viewed as a compact representation of a proof in Hoare Logic: the assertions surrounding each command specify the Hoare triple to be proved for that part of the program using one of the Hoare Logic rules, and the structure of the program itself shows how to assemble all these individual steps into a proof for the whole program.

Example: Swapping

Consider the following program, which swaps the values of two variables using addition and subtraction (instead of by assigning to a temporary variable).
       X := X + Y;
       Y := X - Y;
       X := X - Y We can give a proof, in the form of decorations, that this program is correct -- i.e., it really swaps X and Y -- as follows.

Example: Simple Conditionals

Here's a simple program using conditionals, along with a possible specification:
     {{ True }}
       if X ≤ Y then
         Z := Y - X
       else
         Z := X - Y
       end
     {{ Z + X = Y ∨ Z + Y = X }} Let's turn it into a decorated program...

Example: Reduce to Zero

Here is a very simple while loop with a simple specification:
        {{ True }}
          while (X ≠ 0) do
            X := X - 1
          end
        {{ X = 0 }}

Example: Division

Let's do one more example of simple reasoning about a loop. The following Imp program calculates the integer quotient and remainder of parameters m and n.
       X := m;
       Y := 0;
       while n ≤ X do
         X := X - n;
         Y := Y + 1
       end; If 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:
      {{ True }}
        X := m;
        Y := 0;
        while n ≤ X do
          X := X - n;
          Y := Y + 1
        end
      {{ n × Y + X = m ∧ X < n }}

From Decorated Programs to Formal Proofs

From an informal proof in the form of a decorated program, it is "easy in principle" to read off a formal proof using the Coq theorems corresponding to the Hoare Logic rules, but these proofs can be a bit long and fiddly.

For example...

A little more (OK, quite a bit more) tactic fanciness for helping deal with the boring parts of the process of proving assertions:

This makes it pretty easy to verify reduce_to_zero:

This example shows that it is conceptually straightforward to read off the main elements of a formal proof from a decorated program. Indeed, the process is so straightforward that it can be automated, as we will see next.

Formal Decorated Programs

With a little more work, we can formalize the definition of well-formed decorated programs and automate the boring mechanical steps in proving that the decorations are correct.

Syntax

The first thing we need to do is to formalize a variant of the syntax of Imp commands that includes embedded assertions, which we'll call "decorations." We call the new commands decorated commands, or dcoms. 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 -- something like this...

But this would result in very verbose decorated programs with a lot of repeated annotations: even a simple program like skip;skip would be decorated like this,
        {{P}} ({{P}} skip {{P}}) ; ({{P}} skip {{P}}) {{P}} with pre- and post-conditions around each skip, plus identical pre- and post-conditions on the semicolon!

In other words, 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, the formal syntax of decorated commands omits preconditions whenever possible, trying to embed just the postcondition.

• The skip command, for example, is decorated only with its postcondition
        skip {{ Q }} on the assumption that the precondition will be provided by the context.
  We carry the same assumption through the other syntactic forms: each decorated command is assumed to carry its own postcondition within itself but take its precondition from its context in which it is used.

• Sequences d₁ ; d₂ need no additional decorations.
  Why?
  Because inside d₂ there will be a postcondition; this serves as the postcondition of d₁;d₂.
  Similarly, inside d₁ there will also be a postcondition, which additionally serves as the precondition for d₂.

• An assignment X := a is decorated only with its postcondition:
        X := a {{ Q }}

• A conditional if b then d₁ else d₂ is decorated with a postcondition for the entire statement, as well as preconditions for each branch:
        if b then {{ P₁ }} d₁ else {{ P₂ }} d₂ end {{ Q }}

• A loop while b do d end is decorated with its postcondition and a precondition for the body:
        while b do {{ P }} d end {{ Q }} The postcondition embedded in d serves as the loop invariant.

• Implications ->> can be added as decorations either for a precondition
        ->> {{ P }} d or for a postcondition
        d ->> {{ Q }} The former is waiting for another precondition to be supplied by the context (e.g., {{ P'}} ->> {{ P }} d); the latter relies on the postcondition already embedded in d.

Putting this all together gives us the formal syntax of decorated commands:

(We then need to redefine all our Notations to get nice concrete syntax for dcom.)

To provide the initial precondition that goes at the very top of a decorated program, we introduce a new type decorated:

An example decorated program that decrements X to 0:

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

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

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

For example:

The outer Hoare triple of a decorated program is just a Prop; thus, to show that it is valid, we need to produce a proof of this proposition. We will do this by extracting "proof obligations" from the decorations sprinkled through the program. These obligations are often called verification conditions, because they are the facts that must be verified to see that the decorations are locally consistent and thus constitute a proof of validity of the outer triple.

Extracting Verification Conditions

The function verification_conditions takes a decorated command d together with a precondition P and returns a proposition that, if it can be proved, implies that the triple
     {{P}} erase d {{post d}} is valid. It does this by walking over d and generating a big conjunction that includes

• local consistency checks for each form of command, plus
• uses of ->> to bridge the gap between the assertions found inside a decorated command and the assertions imposed by the precondition from its context; these uses correspond to applications of the consequence rule.

Local consistency is defined as follows...

• The decorated command
          skip {{Q}} is locally consistent with respect to a precondition P if P ->> Q.

• The sequential composition of d₁ and d₂ is locally consistent with respect to P if d₁ is locally consistent with respect to P and d₂ is locally consistent with respect to the postcondition of d₁.

• An assignment
          X := a {{Q}} is locally consistent with respect to a precondition P if:
          P ->> Q [X ⊢> a]

• A conditional
        if b then {{P₁}} d₁ else {{P₂}} d₂ end {{Q}} is locally consistent with respect to precondition P if
  (1) P ∧ b ->> P₁
  (2) P ∧ ¬b ->> P₂
  (3) d₁ is locally consistent with respect to P₁
  (4) d₂ is locally consistent with respect to P₂
  (5) post d₁ ->> Q
  (6) post d₂ ->> Q

• A loop
        while b do {{Q}} d end {{R}} is locally consistent with respect to precondition P if:
  (1) P ->> post d
  (2) post d ∧ b ->> Q
  (3) post d ∧ ¬b ->> R
  (4) d is locally consistent with respect to Q

• A command with an extra assertion at the beginning
         --> {{Q}} d is locally consistent with respect to a precondition P if:
  (1) P ->> Q
  (1) d is locally consistent with respect to Q

• A command with an extra assertion at the end
           d ->> {{Q}} is locally consistent with respect to a precondition P if:
  (1) d is locally consistent with respect to P
  (2) post d ->> Q

With all this in mind, we can write is a verification condition generator that takes a decorated command and reads off a proposition saying that all its decorations are locally consistent. Formally, since a decorated command is "waiting for its precondition" the main VC generator takes a dcom plus a given predondition as arguments.

The following key theorem states that verification_conditions does its job correctly. Not surprisingly, each of the Hoare Logic rules gets used at some point in the proof.

Now that all the pieces are in place, we can define what it means to verify an entire program.

This brings us to the main theorem of this section:

More Automation

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

Fortunately, our verify_assertion tactic can generally take care of most or all of them.

To automate the overall process of verification, we can use verification_correct to extract the verification conditions, use verify_assertion to verify them as much as it can, and finally tidy up any remaining bits by hand.

Here's the final, formal proof that dec_while is correct.

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:
           {{ X = m ∧ Y = n }}
             while X ≠ 0 do
               Y := Y - 1;
               X := X - 1
             end
           {{ Y = n - m }}

To verify this program, we need to find an invariant Inv for the loop. As a first step we can leave Inv 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:
        (1) {{ X = m ∧ Y = n }} ->> (a)
        (2) {{ Inv }}
                 while X ≠ 0 do
        (3) {{ Inv ∧ X ≠ 0 }} ->> (c)
        (4) {{ Inv [X ⊢> X-1] [Y ⊢> Y-1] }}
                   Y := Y - 1;
        (5) {{ Inv [X ⊢> X-1] }}
                   X := X - 1
        (6) {{ Inv }}
                 end
        (7) {{ Inv ∧ ¬(X ≠ 0) }} ->> (b)
        (8) {{ Y = n - m }}

By examining this skeleton, we can see that any valid Inv 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 a single iteration of the loop, assuming that the loop guard also evaluates to true, i.e., (3) must imply (4).

Example: Parity

Here is a cute way of computing the parity of a value initially stored in X, due to Daniel Cristofani.
       {{ X = m }}
         while 2 ≤ X do
           X := X - 2
         end
       {{ X = parity m }} The 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:
    {{ X=m }}
      Z := 0;
      while (Z+1)*(Z+1) ≤ X do
        Z := Z+1
      end
    {{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }}

Example: Squaring

Here is a program that squares X by repeated addition:
  {{ X = m }}
    Y := 0;
    Z := 0;
    while Y ≠ X do
      Z := Z + X;
      Y := Y + 1
    end
  {{ Z = m×m }}

Weakest Preconditions (Optional)

A useless (though valid) Hoare triple:
      {{ False }} X := Y + 1 {{ X ≤ 5 }} A better precondition:
      {{ Y ≤ 4 ∧ Z = 0 }} X := Y + 1 {{ X ≤ 5 }} The best precondition:
      {{ Y ≤ 4 }} X := Y + 1 {{ X ≤ 5 }} Assertion Y ≤ 4 is a weakest precondition of command X := Y + 1 with respect to postcondition X ≤ 5. Think of weakest here as meaning "easiest to satisfy": a weakest precondition is one that as many states as possible can satisfy.

P is a weakest precondition of command c for postcondition Q if

• P is a precondition, that is, {{P}} c {{Q}}; and
• P is at least as weak as all other preconditions, that is, if {{P'}} c {{Q}} then P' ->> P.

Exercise: 1 star, standard, optional (wp)

What are weakest preconditions of the following commands for the following postconditions?
  1) {{ ? }} skip {{ X = 5 }}

  2) {{ ? }} X := Y + Z {{ X = 5 }}

  3) {{ ? }} X := Y {{ X = Y }}

  4) {{ ? }}
     if X = 0 then Y := Z + 1 else Y := W + 2 end
     {{ Y = 5 }}

  5) {{ ? }}
     X := 5
     {{ X = 0 }}

  6) {{ ? }}
     while true do X := 0 end
     {{ X = 0 }}