Decorated Programs

The beauty of Hoare Logic is that it is compositional: the structure of proofs exactly follows the structure of programs. As we saw in Hoare, 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:
    X := m;
    Z := p;
    while ~(X = 0) do
      Z := Z - 1;
      X := X - 1
    end

Here is one possible specification for this program:
      {{ True }}
    X := m;
    Z := p;
    while ~(X = 0) do
      Z := Z - 1;
      X := X - 1
    end
      {{ Z = p - m }} Note the parameters m and p, which stand for fixed-but-arbitrary numbers. Formally, they are simply Coq variables of type nat.

Here is a decorated version of the 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 text interleaved with assertions (or possibly multiple assertions separated by implications).

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 X := a is locally consistent with respect to a precondition of the form P [X ⊢> a] and the postcondition P:
            {{ P [X ⊢> a] }}
            X := a
            {{ P }}

• A conditional is locally consistent with respect to assertions P and Q 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 }}
            if b then
              {{ P ∧ b }}
              c₁
              {{ Q }}
            else
              {{ P ∧ ¬b }}
              c₂
              {{ Q }}
            end
            {{ 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 with respect to assertions P ∧ b and P:
            {{ 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).
       X := X + Y;
       Y := X - Y;
       X := X - Y We can prove (informally) 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:
         {{ 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 }}

From an informal proof in the form of a decorated program, it is easy to read off a formal proof using the Coq theorems corresponding to the Hoare Logic rules. Note that we do not unfold the definition of hoare_triple anywhere in this proof: the point of the game is to use the Hoare rules as a self-contained logic for reasoning about programs.

In Hoare we introduced a series of tactics named assn_auto to automate proofs involving just assertions. We can try using the most advanced of those tactics to streamline the previous proof:

Automation to the rescue!

All that automation makes it easy to verify reduce_to_zero':

Example: Division

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 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 }}

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 each iteration of the loop (given that the loop guard evaluates to true), 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).
         {{ X = m }}
       while 2 ≤ X do
         X := X - 2
       end
         {{ X = parity m }} 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:
      {{ 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 }}

Formal Decorated Programs (Advanced)

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

Decorated commands contain assertions mostly just as postconditions, omitting preconditions where possible and letting the context supply them. The alternative--decorating every command with both a pre- and postcondition--would be too heavyweight. E.g., skip; skip would become:
        {{P}} ({{P}} skip {{P}}) ; ({{P}} skip {{P}}) {{P}}, Specifically, we decorate as follows:

• Command skip is decorated only with its postcondition, as skip {{ Q }}.
• Sequence d₁ ; d₂ contains no additional decoration. Inside d₂ there will be a postcondition; that serves as the postcondition of d₁ ; d₂. Inside d₁ there will also be a postcondition; it additionally serves as the precondition for d₂.
• Assignment X := a is decorated only with its postcondition, as X := a {{ Q }}.
• If statement if b then d₁ else d₂ is decorated with a postcondition for the entire statement, as well as preconditions for each branch, as if b then {{ P₁ }} d₁ else {{ P₂ }} d₂ end {{ Q }}.
• While loop while b do d end is decorated with its postcondition and a precondition for the body, as while b do {{ P }} d end {{ Q }}. The postcondition inside d serves as the loop invariant.
• Implications ->> are added as decorations for a precondition as ->> {{ P }} d, or for a postcondition as d ->> {{ Q }}. The former is waiting for another precondition to eventually be supplied, e.g., {{ P'}} ->> {{ P }} d, and the latter relies on the postcondition already embedded in d.

DCPre is used to provide the weakened precondition from the rule of consequence. To provide the initial precondition at the very top of the program, we use Decorated:

To avoid clashing with the existing Notation definitions for ordinary commands, we introduce these notations in a custom entry notation called dcom.

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 straightforward to extract the precondition and postcondition from a decorated program.

When is a decorated program correct?

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, because they are the facts that must be verified to see that the decorations are logically consistent and thus constitute a proof of correctness.

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. It does this by walking over d and generating a big conjunction that includes

• all the local consistency checks, plus
• many uses of ->> to bridge the gap between (i) assertions found inside decorated commands and (ii) assertions used by the local consistency checks. These uses correspond applications of the consequence rule.

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.

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. Our verify_assn can often take care of them.

Automation

To automate the entire process of verification, we can use verification_correct to extract the verification conditions, then use verify_assn to verify them (if it can).

Let's use all this automation to verify formal decorated programs corresponding to some of the informal ones we have seen.

Slow Subtraction

Swapping Using Addition and Subtraction

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