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.

These local consistency conditions essentially describe a procedure for verifying the correctness of a given proof. This verification involves checking that every single command is locally consistent with the accompanying assertions. If we are instead interested in finding a proof for a given specification, we need to discover the right assertions. This can be done in an almost mechanical way, with the exception of finding loop invariants. In the remainder of this section we explain in detail how to construct decorations for several short programs, all of which are loop-free or have simple loop invariants. We defer a full discussion of finding loop invariants to the next section.

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.
    (1) {{ X = m ∧ Y = n }} ->>
    (2) {{ (X + Y) - ((X + Y) - Y) = n ∧ (X + Y) - Y = m }}
           X := X + Y;
    (3) {{ X - (X - Y) = n ∧ X - Y = m }}
           Y := X - Y;
    (4) {{ X - Y = n ∧ Y = m }}
           X := X - Y
    (5) {{ X = n ∧ Y = m }}

The decorations can be constructed as follows:

• We begin with the undecorated program (the unnumbered lines).
• We add the specification -- i.e., the outer precondition (1) and postcondition (5). In the precondition, we use parameters m and n to remember the initial values of variables X and Y so that we can refer to them in the postcondition (5).
• We work backwards, mechanically, starting from (5) and proceeding until we get to (2). At each step, we obtain the precondition of the assignment from its postcondition by substituting the assigned variable with the right-hand-side of the assignment. For instance, we obtain (4) by substituting X with X - Y in (5), and we obtain (3) by substituting Y with X - Y in (4).

Finally, we verify that (1) logically implies (2) -- i.e., that the step from (1) to (2) is a valid use of the law of consequence. For this we substitute X by m and Y by n and calculate as follows:
            (m + n) - ((m + n) - n) = n ∧ (m + n) - n = m
            (m + n) - m = n ∧ m = m
            n = n ∧ m = m

Note that, since we are working with natural numbers rather than fixed-width machine integers, we don't need to worry about the possibility of arithmetic overflow anywhere in this argument. This makes life quite a bit simpler!

Example: Simple Conditionals

Here is a simple decorated program using conditionals:
      (1) {{True}}
            if X ≤ Y then
      (2) {{True ∧ X ≤ Y}} ->>
      (3) {{(Y - X) + X = Y ∨ (Y - X) + Y = X}}
              Z := Y - X
      (4) {{Z + X = Y ∨ Z + Y = X}}
            else
      (5) {{True ∧ ~(X ≤ Y) }} ->>
      (6) {{(X - Y) + X = Y ∨ (X - Y) + Y = X}}
              Z := X - Y
      (7) {{Z + X = Y ∨ Z + Y = X}}
            end
      (8) {{Z + X = Y ∨ Z + Y = X}}

These decorations were constructed as follows:

• We start with the outer precondition (1) and postcondition (8).
• We follow the format dictated by the hoare_if rule and copy the postcondition (8) to (4) and (7). We conjoin the precondition (1) with the guard of the conditional to obtain (2). We conjoin (1) with the negated guard of the conditional to obtain (5).
• In order to use the assignment rule and obtain (3), we substitute Z by Y - X in (4). To obtain (6) we substitute Z by X - Y in (7).
• Finally, we verify that (2) implies (3) and (5) implies (6). Both of these implications crucially depend on the ordering of X and Y obtained from the guard. For instance, knowing that X ≤ Y ensures that subtracting X from Y and then adding back X produces Y, as required by the first disjunct of (3). Similarly, knowing that ¬ (X ≤ Y) ensures that subtracting Y from X and then adding back Y produces X, as needed by the second disjunct of (6). Note that n - m + m = n does not hold for arbitrary natural numbers n and m (for example, 3 - 5 + 5 = 5).

Exercise: 2 stars, standard (if_minus_plus_reloaded)

Fill in valid decorations for the following program:
       {{ True }}
      if X ≤ Y then
          {{ }} ->>
          {{ }}
        Z := Y - X
          {{ }}
      else
          {{ }} ->>
          {{ }}
        Y := X + Z
          {{ }}
      end
        {{ Y = X + Z }}

Briefly justify each use of ->>.

Example: Reduce to Zero

Here is a while loop that is so simple that True suffices as a loop invariant.
        (1) {{ True }}
               while ~(X = 0) do
        (2) {{ True ∧ X ≠ 0 }} ->>
        (3) {{ True }}
                 X := X - 1
        (4) {{ True }}
               end
        (5) {{ True ∧ ~(X ≠ 0) }} ->>
        (6) {{ X = 0 }}

The decorations can be constructed as follows:

• Start with the outer precondition (1) and postcondition (6).
• Following the format dictated by the hoare_while rule, we copy (1) to (4). We conjoin (1) with the guard to obtain (2). The guard is a Boolean expression ~(X = 0), which for simplicity we express in assertion (2) as X ≠ 0. We also conjoin (1) with the negation of the guard to obtain (5).
• Because the outer postcondition (6) does not syntactically match (5), we add an implication between them.
• Using the assignment rule with assertion (4), we trivially substitute and obtain assertion (3).
• We add the implication between (2) and (3).

Finally we check that the implications do hold; both are trivial. 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:

Let's introduce a (much) more sophisticated tactic that will help with proving assertions throughout the rest of this chapter. You don't need to understand the details of it. Briefly, it uses split repeatedly to turn all the conjunctions into separate subgoals, tries to use several theorems about booleans and (in)equalities, then uses eauto and omega to finish off as many subgoals as possible. What's left after verify does its thing is just the "interesting parts" of checking that the assertions correct --which might be nothing.

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. In order to give a specification to this program we need to remember that dividing m by n produces a remainder X and a quotient Y such that n × Y + X = m ∧ X < n. It turns out that we get lucky with this program and don't have to think very hard about the loop invariant: the invariant is just the first conjunct n × Y + X = m, and we can use this to decorate the program.
      (1) {{ True }} ->>
      (2) {{ n × 0 + m = m }}
           X := m;
      (3) {{ n × 0 + X = m }}
           Y := 0;
      (4) {{ n × Y + X = m }}
           while n ≤ X do
      (5) {{ n × Y + X = m ∧ n ≤ X }} ->>
      (6) {{ n × (Y + 1) + (X - n) = m }}
             X := X - n;
      (7) {{ n × (Y + 1) + X = m }}
             Y := Y + 1
      (8) {{ n × Y + X = m }}
           end
      (9) {{ n × Y + X = m ∧ ¬(n ≤ X) }} ->>
     (10) {{ n × Y + X = m ∧ X < n }}

Assertions (4), (5), (8), and (9) are derived mechanically from the invariant and the loop's guard. Assertions (8), (7), and (6) are derived using the assignment rule going backwards from (8) to (6). Assertions (4), (3), and (2) are again backwards applications of the assignment rule. Now that we've decorated the program it only remains to check that the uses of the consequence rule are correct -- i.e., that (1) implies (2), that (5) implies (6), and that (9) implies (10). This is indeed the case:

• (1) ->> (2): trivial, by algebra.
• (5) ->> (6): because n ≤ X, we are guaranteed that the subtraction in (6) does not get zero-truncated. We can therefore rewrite (6) as n × Y + n + X - n and cancel the ns, which results in the left conjunct of (5).
• (9) ->> (10): if ¬ (n ≤ X) then X < n. That's straightforward from high-school algebra.

So, we have a valid decorated program.

Finding Loop Invariants

Once the outermost precondition and postcondition are chosen, the only creative part in verifying programs 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 the *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.
• Strengthening the *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 each iteration of the loop (given that the loop guard 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 an 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 an invariant did the job. So 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, condition (b) is wrong, i.e., 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 invariant so that it implies the postcondition (8). One simple way to do this is to let the invariant be the postcondition. So let's return to our skeleton, instantiate Inv with Y = n - m, and check 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 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 an invariant! To do better, we need to generalize (8) 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.)

Exercise: Slow Assignment

Exercise: 2 stars, standard (slow_assignment)

A roundabout way of assigning a number currently stored in X to the variable Y is to start Y at 0, then decrement X until it hits 0, incrementing Y at each step. Here is a program that implements this idea:
        {{ X = m }}
      Y := 0;
      while ~(X = 0) do
        X := X - 1;
        Y := Y + 1
      end
        {{ Y = m }}

Write an informal decorated program showing that this procedure is correct, and justify each use of ->>.

Exercise: Slow Addition

Exercise: 3 stars, standard, optional (add_slowly_decoration)

The following program adds the variable X into the variable Z by repeatedly decrementing X and incrementing Z.
      while ~(X = 0) do
         Z := Z + 1;
         X := X - 1
      end

Following the pattern of the subtract_slowly example above, pick a precondition and postcondition that give an appropriate specification of add_slowly; then (informally) decorate the program accordingly, and justify each use of ->>.

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:

The postcondition does not hold at the beginning of the loop, since m = parity m does not hold for an arbitrary m, so we cannot use that as an invariant. To find an invariant that works, let's think a bit about what this loop does. On each iteration it decrements X by 2, which preserves the parity of X. So the parity of X does not change, i.e., it is invariant. The initial value of X is m, so the parity of X is always equal to the parity of m. Using parity X = parity m as an invariant we obtain the following decorated program:
        {{ X = m }} ->> (a - OK)
        {{ parity X = parity m }}
      while 2 ≤ X do
          {{ parity X = parity m ∧ 2 ≤ X }} ->> (c - OK)
          {{ parity (X-2) = parity m }}
        X := X - 2
          {{ parity X = parity m }}
      end
        {{ parity X = parity m ∧ ~(2 ≤ X) }} ->> (b - OK)
        {{ X = parity m }}

With this invariant, conditions (a), (b), and (c) are all satisfied. For verifying (b), we observe that, when X < 2, we have parity X = X (we can easily see this in the definition of parity). For verifying (c), we observe that, when 2 ≤ X, we have parity X = parity (X-2).

Exercise: 3 stars, standard, optional (parity_formal)

Translate the above informal decorated program into a formal proof in Coq. Your proof should use the Hoare logic rules and should not unfold hoare_triple. Refer to reduce_to_zero for an example. To formally state the invariant, you will need the ap operator to apply parity to an Imp variable --e.g., ap parity X. After using verify_assn, you will be left needing to prove some facts about parity. The following lemmas will be helpful, as will leb_complete and leb_correct.

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 above, we can try to use the postcondition as a candidate 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 ∧ (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, if 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 add the fact that it doesn't change to the loop invariant.

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 invariant. The other thing that we know is often useful in the invariant is the postcondition, so let's add that too, leading to the candidate 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 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 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 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 invariants.

Exercise: Factorial

Exercise: 3 stars, standard (factorial)

Recall that n! denotes the factorial of n (i.e., n! = 1*2*...*n). Here is an Imp program that calculates the factorial of the number initially stored in the variable X and puts it in the variable Y:
    {{ X = m }}
  Y := 1 ;
  while ~(X = 0)
  do
     Y := Y × X ;
     X := X - 1
  end
    {{ Y = m! }}

Fill in the blanks in following decorated program. 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.
    {{ X = m }} ->>
    {{ }}
  Y := 1;
    {{ }}
  while ~(X = 0)
  do {{ }} ->>
       {{ }}
     Y := Y × X;
       {{ }}
     X := X - 1
       {{ }}
  end
    {{ }} ->>
    {{ Y = m! }}

Briefly justify each use of ->>.

Exercise: Min

Exercise: 3 stars, standard (Min_Hoare)

Fill in valid decorations for the following program, and justify the uses of ->>. As in factorial, be careful about natural numbers, especially subtraction. In your justifications, you may rely on the following facts about min:
  Lemma lemma1 : ∀ x y,
    (x<>0 ∧ y<>0) → min x y ≠ 0.
  Lemma lemma2 : ∀ x y,
    min (x-1) (y-1) = (min x y) - 1.

plus standard high-school algebra, as always.
  {{ True }} ->>
  {{ }}
  X := a;
  {{ }}
  Y := b;
  {{ }}
  Z := 0;
  {{ }}
  while ~(X = 0) && ~(Y = 0) do
    {{ }} ->>
    {{ }}
    X := X - 1;
    {{ }}
    Y := Y - 1;
    {{ }}
    Z := Z + 1
    {{ }}
  end
  {{ }} ->>
  {{ Z = min a b }}

Exercise: 3 stars, standard (two_loops)

Here is a very 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 filling in the blanks in the following decorated program.
      {{ True }} ->>
      {{ }}
    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
      {{ }} ->>
      {{ Z = a + b + c }}

Exercise: Power Series

Exercise: 4 stars, standard, optional (dpow2_down)

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

Write a decorated program for this, and justify each use of ->>.

Weakest Preconditions (Optional)

Some preconditions are more interesting than others. For example,
      {{ False }} X := Y + 1 {{ X ≤ 5 }}

is not very interesting: although it is perfectly valid Hoare triple, 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 is this one:
      {{ Y ≤ 4 }} X := Y + 1 {{ X ≤ 5 }}

Assertion Y ≤ 4 is the weakest precondition of command X ::= Y + 1 for 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.

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

Exercise: 3 stars, advanced, optional (is_wp_formal)

Prove formally, using the definition of 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.

Formal Decorated Programs (Advanced)

Our informal conventions for decorated programs amount to a way of displaying Hoare triples, in which commands are annotated with enough embedded assertions that checking the validity of a triple is reduced to simple logical and algebraic calculations showing that some assertions imply others. In this section, we show that this presentation style can actually be made completely formal -- and indeed that checking the validity of decorated programs can mostly be automated.

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. 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
        {{P}} ({{P}} skip {{P}}) ; ({{P}} skip {{P}}) {{P}},

with pre- and post-conditions on each skip, plus identical pre- and post-conditions on the semicolon! 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, we'll omit preconditions whenever possible, trying to embed just the postcondition. 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.

Recall that you can Set Printing All to see how all that notation is desugared.

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.

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

Division

Parity

There are actually several ways to phrase the loop invariant for this program. Here is one natural one, which leads to a rather long proof: