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.

Similarly, here is the formal decorated program for the "swapping by adding and subtracting" example that we saw earlier.

And here is the formal decorated version of the "positive difference" program from earlier:

Exercise: 3 stars, standard (reverse_incorrect)

Prove that the reverse implication of theorem verification_correct is not correct.

Exercise: 2 stars, standard, optional (if_minus_plus_correct)

Here is a skeleton of the formal decorated version of the if_minus_plus program that we saw earlier. Replace all occurrences of FILL_IN_HERE with appropriate assertions and fill in the proof (which should be just as straightforward as in the examples above).

Exercise: 2 stars, standard (div_mod_outer_triple_valid)

Fill in appropriate assertions for the division program from last week and prove it with the verify tactic.

Finding Loop Invariants

Once the outermost precondition and postcondition are chosen, the only creative part of a verifying program using Hoare Logic is finding the right loop invariants. The reason this is difficult is the same as the reason that inductive mathematical proofs are:

• Strengthening a loop invariant means that you have a stronger assumption to work with when trying to establish the postcondition of the loop body, but it also means that the loop body's postcondition is stronger and thus harder to prove.
• Similarly, strengthening an induction hypothesis means that you have a stronger assumption to work with when trying to complete the induction step of the proof, but it also means that the statement being proved inductively is stronger and thus harder to prove.

This section explains how to approach the challenge of finding loop invariants through a series of examples and exercises.

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).

These conditions are actually independent of the particular program and specification we are considering: every loop invariant has to satisfy them. One way to find a loop invariant that simultaneously satisfies these three conditions is by using an iterative process: start with a "candidate" invariant (e.g., a guess or a heuristic choice) and check the three conditions above; if any of the checks fails, try to use the information that we get from the failure to produce another -- hopefully better -- candidate invariant, and repeat. For instance, in the reduce-to-zero example above, we saw that, for a very simple loop, choosing True as a loop invariant did the job. Maybe it will work here too. To find out, let's try instantiating Inv with True in the skeleton above and see what we get...
        (1) {{ X = m ∧ Y = n }} ->> (a - OK)
        (2) {{ True }}
                 while X ≠ 0 do
        (3) {{ True ∧ X ≠ 0 }} ->> (c - OK)
        (4) {{ True }}
                   Y := Y - 1;
        (5) {{ True }}
                   X := X - 1
        (6) {{ True }}
                 end
        (7) {{ True ∧ ~(X ≠ 0) }} ->> (b - WRONG!)
        (8) {{ Y = n - m }} While conditions (a) and (c) are trivially satisfied, (b) is wrong: it is not the case that True ∧ X = 0 (7) implies Y = n - m (8). In fact, the two assertions are completely unrelated, so it is very easy to find a counterexample to the implication (say, Y = X = m = 0 and n = 1). If we want (b) to hold, we need to strengthen the loop invariant so that it implies the postcondition (8). One simple way to do this is to let the loop invariant be the postcondition. So let's return to our skeleton, instantiate Inv with Y = n - m, and try checking conditions (a) to (c) again.
    (1) {{ X = m ∧ Y = n }} ->> (a - WRONG!)
    (2) {{ Y = n - m }}
             while X ≠ 0 do
    (3) {{ Y = n - m ∧ X ≠ 0 }} ->> (c - WRONG!)
    (4) {{ Y - 1 = n - m }}
               Y := Y - 1;
    (5) {{ Y = n - m }}
               X := X - 1
    (6) {{ Y = n - m }}
             end
    (7) {{ Y = n - m ∧ ~(X ≠ 0) }} ->> (b - OK)
    (8) {{ Y = n - m }} This time, condition (b) holds trivially, but (a) and (c) are broken. Condition (a) requires that (1) X = m ∧ Y = n implies (2) Y = n - m. If we substitute Y by n we have to show that n = n - m for arbitrary m and n, which is not the case (for instance, when m = n = 1). Condition (c) requires that n - m - 1 = n - m, which fails, for instance, for n = 1 and m = 0. So, although Y = n - m holds at the end of the loop, it does not hold from the start, and it doesn't hold on each iteration; it is not a correct loop invariant. This failure is not very surprising: the variable Y changes during the loop, while m and n are constant, so the assertion we chose didn't have much chance of being a loop invariant! To do better, we need to generalize (7) to some statement that is equivalent to (8) when X is 0, since this will be the case when the loop terminates, and that "fills the gap" in some appropriate way when X is nonzero. Looking at how the loop works, we can observe that X and Y are decremented together until X reaches 0. So, if X = 2 and Y = 5 initially, after one iteration of the loop we obtain X = 1 and Y = 4; after two iterations X = 0 and Y = 3; and then the loop stops. Notice that the difference between Y and X stays constant between iterations: initially, Y = n and X = m, and the difference is always n - m. So let's try instantiating Inv in the skeleton above with Y - X = n - m.
    (1) {{ X = m ∧ Y = n }} ->> (a - OK)
    (2) {{ Y - X = n - m }}
             while X ≠ 0 do
    (3) {{ Y - X = n - m ∧ X ≠ 0 }} ->> (c - OK)
    (4) {{ (Y - 1) - (X - 1) = n - m }}
               Y := Y - 1;
    (5) {{ Y - (X - 1) = n - m }}
               X := X - 1
    (6) {{ Y - X = n - m }}
             end
    (7) {{ Y - X = n - m ∧ ~(X ≠ 0) }} ->> (b - OK)
    (8) {{ Y = n - m }} Success! Conditions (a), (b) and (c) all hold now. (To verify (c), we need to check that, under the assumption that X ≠ 0, we have Y - X = (Y - 1) - (X - 1); this holds for all natural numbers X and Y.) Here is the final version of the decorated program:

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) }} As we did before, we can try to use the postcondition as a candidate loop invariant, obtaining the following decorated program:
    (1) {{ X=m }} ->> (a - second conjunct of (2) WRONG!)
    (2) {{ 0*0 ≤ m ∧ m<(0+1)*(0+1) }}
            Z := 0
    (3) {{ Z×Z ≤ m ∧ m<(Z+1)*(Z+1) }};
            while (Z+1)*(Z+1) ≤ X do
    (4) {{ Z×Z≤m ∧ m<(Z+1)*(Z+1)
                             ∧ (Z+1)*(Z+1)<=X }} ->> (c - WRONG!)
    (5) {{ (Z+1)*(Z+1)<=m ∧ m<((Z+1)+1)*((Z+1)+1) }}
              Z := Z+1
    (6) {{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }}
            end
    (7) {{ Z×Z≤m ∧ m<(Z+1)*(Z+1) ∧ ~((Z+1)*(Z+1)<=X) }} ->> (b - OK)
    (8) {{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }} This didn't work very well: conditions (a) and (c) both failed. Looking at condition (c), we see that the second conjunct of (4) is almost the same as the first conjunct of (5), except that (4) mentions X while (5) mentions m. But note that X is never assigned in this program, so we should always have X=m. We didn't propagate this information from (1) into the loop invariant, but we could! Also, we don't need the second conjunct of (8), since we can obtain it from the negation of the guard -- the third conjunct in (7) -- again under the assumption that X=m. This allows us to simplify a bit. So we now try X=m ∧ Z×Z ≤ m as the loop invariant:
    {{ X=m }} ->> (a - OK)
    {{ X=m ∧ 0*0 ≤ m }}
      Z := 0
                 {{ X=m ∧ Z×Z ≤ m }};
      while (Z+1)*(Z+1) ≤ X do
                 {{ X=m ∧ Z×Z≤m ∧ (Z+1)*(Z+1)<=X }} ->> (c - OK)
                 {{ X=m ∧ (Z+1)*(Z+1)<=m }}
        Z := Z + 1
                 {{ X=m ∧ Z×Z≤m }}
      end
    {{ X=m ∧ Z×Z≤m ∧ ~((Z+1)*(Z+1)<=X) }} ->> (b - OK)
    {{ Z×Z≤m ∧ m<(Z+1)*(Z+1) }} This works, since conditions (a), (b), and (c) are now all trivially satisfied. Very often, when a variable is used in a loop in a read-only fashion (i.e., it is referred to by the program or by the specification and it is not changed by the loop), it is necessary to record the fact that it doesn't change in the loop invariant.

Exercise: 2 stars, standard (sqrt_dec)

Translate the above informal decorated program into a formal one and prove it correct.

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 }} The first thing to note is that the loop reads X but doesn't change its value. As we saw in the previous example, it can be a good idea in such cases to add X = m to the loop invariant. The other thing that we know is often useful in the loop invariant is the postcondition, so let's add that too, leading to the candidate loop invariant Z = m × m ∧ X = m.
    {{ X = m }} ->> (a - WRONG)
    {{ 0 = m×m ∧ X = m }}
      Y := 0
                   {{ 0 = m×m ∧ X = m }};
      Z := 0
                   {{ Z = m×m ∧ X = m }};
      while Y ≠ X do
                   {{ Z = m×m ∧ X = m ∧ Y ≠ X }} ->> (c - WRONG)
                   {{ Z+X = m×m ∧ X = m }}
        Z := Z + X
                   {{ Z = m×m ∧ X = m }};
        Y := Y + 1
                   {{ Z = m×m ∧ X = m }}
      end
    {{ Z = m×m ∧ X = m ∧ ~(Y ≠ X) }} ->> (b - OK)
    {{ Z = m×m }} Conditions (a) and (c) fail because of the Z = m×m part. While Z starts at 0 and works itself up to m×m, we can't expect Z to be m×m from the start. If we look at how Z progresses in the loop, after the 1st iteration Z = m, after the 2nd iteration Z = 2*m, and at the end Z = m×m. Since the variable Y tracks how many times we go through the loop, this leads us to derive a new loop invariant candidate: Z = Y×m ∧ X = m.
    {{ X = m }} ->> (a - OK)
    {{ 0 = 0*m ∧ X = m }}
      Y := 0
                    {{ 0 = Y×m ∧ X = m }};
      Z := 0
                    {{ Z = Y×m ∧ X = m }};
      while Y ≠ X do
                    {{ Z = Y×m ∧ X = m ∧ Y ≠ X }} ->> (c - OK)
                    {{ Z+X = (Y+1)*m ∧ X = m }}
        Z := Z + X
                    {{ Z = (Y+1)*m ∧ X = m }};
        Y := Y + 1
                    {{ Z = Y×m ∧ X = m }}
      end
    {{ Z = Y×m ∧ X = m ∧ ~(Y ≠ X) }} ->> (b - OK)
    {{ Z = m×m }} This new loop invariant makes the proof go through: all three conditions are easy to check. It is worth comparing the postcondition Z = m×m and the Z = Y×m conjunct of the loop invariant. It is often the case that one has to replace parameters with variables -- or with expressions involving both variables and parameters, like m - Y -- when going from postconditions to loop invariants. ☐

Exercise: Two Loops

Exercise: 3 stars, standard (two_loops)

Here is a pretty inefficient way of adding 3 numbers:
     X := 0;
     Y := 0;
     Z := c;
     while X ≠ a do
       X := X + 1;
       Z := Z + 1
     end;
     while Y ≠ b do
       Y := Y + 1;
       Z := Z + 1
     end Show that it does what it should by completing the following decorated program. If done correctly, the verify tactic should be able to find the proof automatically.

Exercise: Minimum

Exercise: 3 stars, standard (minimum_correct)

Fill in decorations for the following program and prove them correct. Be careful about mathematical reasoning involving natural numbers, especially subtraction. Also, remember that applications of Coq functions in assertions need an ap or ap₂ to be parsed correctly. E.g., min a b needs to be written ap₂ min a b in an assertion. You may find andb_true_eq useful (perhaps after using symmetry to get an equality the right way around).

Exercise: Factorial

Exercise: 4 stars, advanced, optional (factorial_correct)

Recall that n! denotes the factorial of n (i.e., n! = 1*2*...*n). Formally, the factorial function is defined recursively in the Coq standard library in a way that is equivalent to the following:
    Fixpoint fact (n : nat) : nat :=
      match n with
      | O ⇒ 1
      | S n' ⇒ n × (fact n')
      end.

First, write the Imp program factorial that calculates the factorial of the number initially stored in the variable X and puts it in the variable Y. Using your definition factorial as a guide, write a formal decorated program factorial_dec that implements the factorial function. Hint: recall the use of ap in assertions to apply a function to an Imp variable. Fill in the blanks and finish the proof of correctness. As with minimum, bear in mind that we are working with natural numbers, for which both division and subtraction can behave differently than with real numbers. Excluding both operations from your loop invariant is advisable! Then state a theorem named factorial_correct that says factorial_dec is correct, and prove the theorem. If all goes well, verify will leave you with just two subgoals, each of which requires establishing some mathematical property of fact, rather than proving anything about your program. Hint: if those two subgoals become tedious to prove, give some thought to how you could restate your assertions such that the mathematical operations are more amenable to manipulation in Coq. For example, recall that 1 + ... is easier to work with than ... + 1.

Exercise: Power Series

Exercise: 4 stars, standard, optional (dpow2)

Here is a program that computes the series: 1 + 2 + 2^2 + ... + 2^m = 2^(m+1) - 1
    X := 0;
    Y := 1;
    Z := 1;
    while X ≠ m do
      Z := 2 × Z;
      Y := Y + Z;
      X := X + 1
    end Turn this into a decorated program and prove it correct.

Some lemmas that you may find useful...

The main correctness theorem:

Exercise: 2 stars, advanced, optional (fib_eqn)

The Fibonacci function is usually written like this:
      Fixpoint fib n :=
        match n with
        | 0 ⇒ 1
        | 1 ⇒ 1
        | _ ⇒ fib (pred n) + fib (pred (pred n))
        end. This doesn't pass Coq's termination checker, but here is a slightly clunkier definition that does:

Prove that fib satisfies the following equation. You will need this as a lemma in the next exercise.

Exercise: 4 stars, advanced, optional (fib)

The following Imp program leaves the value of fib n in the variable Y when it terminates:
    X := 1;
    Y := 1;
    Z := 1;
    while X ≠ 1 + n do
      T := Z;
      Z := Z + Y;
      Y := T;
      X := 1 + X
    end Fill in the following definition of dfib and prove that it satisfies this specification:
      {{ True }} dfib {{ Y = fib n }} You will need many uses of ap in your assertions. If all goes well, your proof will be very brief.

Exercise: 5 stars, advanced, optional (improve_dcom)

The formal decorated programs defined in this section are intended to look as similar as possible to the informal ones defined earlier. If we drop this requirement, we can eliminate almost all annotations, just requiring final postconditions and loop invariants to be provided explicitly. Do this -- i.e., define a new version of dcom with as few annotations as possible and adapt the rest of the formal development leading up to the verification_correct theorem.

Weakest Preconditions

Some preconditions are more interesting than others. For example, the Hoare triple
      {{ False }} X := Y + 1 {{ X ≤ 5 }} is not very interesting: although it is perfectly valid , it tells us nothing useful. Since the precondition isn't satisfied by any state, it doesn't describe any situations where we can use the command X := Y + 1 to achieve the postcondition X ≤ 5. By contrast,
      {{ Y ≤ 4 ∧ Z = 0 }} X := Y + 1 {{ X ≤ 5 }} has a useful precondition: it tells us that, if we can somehow create a situation in which we know that Y ≤ 4 ∧ Z = 0, then running this command will produce a state satisfying the postcondition. However, this precondition is not as useful as it could be, because the Z = 0 clause in the precondition actually has nothing to do with the postcondition X ≤ 5. The most useful precondition for this command is this one:
      {{ Y ≤ 4 }} X := Y + 1 {{ X ≤ 5 }} The assertion Y ≤ 4 is called the weakest precondition of X := Y + 1 with respect to the postcondition 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.

Note that weakest preconditions need not be unique. For example, Y ≤ 4 was a weakest precondition above, but so are the logically equivalent assertions Y < 5, Y ≤ 2 × 2, etc. It is easy to show that any two weakest preconditions P and P' of a command c with respect to postcondition Q are logically equivalent; that is, P <<->> P'.

Exercise: 2 stars, standard (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 }}

Exercise: 3 stars, advanced (is_wp_example)

Prove formally, using the definition of valid_hoare_triple, that Y ≤ 4 is indeed a weakest precondition of X := Y + 1 with respect to postcondition X ≤ 5.

Exercise: 2 stars, advanced, optional (hoare_asgn_weakest)

Show that the precondition in the rule hoare_asgn is in fact the weakest precondition.

Exercise: 2 stars, advanced, optional (hoare_havoc_weakest)

Show that your havoc_pre function from the himp_hoare exercise in the Hoare chapter returns a weakest precondition.