Decorated Programs

霍尔逻辑的美妙之处在于它是 '可组合的': 证明的结构完全遵循程序的结构。 这表明我们可以通过在每个命令上使用适当的断言“装饰”程序来记录证明的基本思想 （非正式地，并省略一些底层的计算细节）。 这样一个 '带装饰的程序（Decorated Program）' 自带一个关于它自身正确性的证明。 例如，考虑以下程序：
    X ::= m;;
    Z ::= p;
    WHILE ~(X = 0) DO
      Z ::= Z - 1;;
      X ::= X - 1
    END

(注意 '参数' m 和 p，它们代表任意给定数字（fixed-but-arbitrary numbers）。 形式上，它们只是 nat 类型的 Coq 变量) 这是这个程序的一个可能的规格说明：
      {{ True }}
    X ::= m;;
    Z ::= p;
    WHILE ~(X = 0) DO
      Z ::= Z - 1;;
      X ::= X - 1
    END
      {{ Z = p - m }}

这是该程序的装饰版本，体现了该规格说明的证明：
      {{ 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 }}

具体地说，一个带装饰的程序包括与断言交错的程序文本（单个断言或可能由蕴含符号分隔的两个断言）。 要检查一个带装饰的程序是否代表一个有效的证明，我们只需检查每个单独的命令是否与其附近的断言在以下各个场景下 '局部一致（Locally Consistent）'：

• 如果 SKIP 的前置条件和后置条件相同，则它是局部一致的:
            {{ P }} SKIP {{ P }}

• 我们说 c₁ 和 c₂ 的顺序组合是局部一致的（相对于断言 P 和 R）， 如果 c₁ 是局部一致的（相对于断言 P 和 Q）并且 c₂ 是局部一致的（相对于断言 Q 和 R）：
            {{ P }} c₁;; {{ Q }} c₂ {{ R }}

• 如果赋值语句的前置条件是其后置条件的适当替换，则该赋值语句是局部一致的：
            {{ P [X ⊢> a] }}
            X ::= a
            {{ P }}

• 我们说一个条件语句是局部一致的 (相对于断言 P 和 Q) ， 如果它的 "then" 和 "else" 两个分支顶部的断言恰好是 P ∧ b 和 P ∧ ¬b， 并且 "then" 分支是局部一致的 (相对于断言 P ∧ b 和 Q) 且 "else" 分支是局部一致的 (相对于断言 P ∧ ¬b 和 Q)：
            {{ P }}
            TEST b THEN
              {{ P ∧ b }}
              c₁
              {{ Q }}
            ELSE
              {{ P ∧ ¬b }}
              c₂
              {{ Q }}
            FI
            {{ Q }}

• 我们说一个前置条件为 P 的 while 循环是局部一致的， 如果它的后置条件是 P ∧ ¬b， 并且如果它循环体的前置条件和后置条件是 P ∧ b 和 P， 并且它的循环体是局部一致的：
            {{ P }}
            WHILE b DO
              {{ P ∧ b }}
              c₁
              {{ P }}
            END
            {{ P ∧ ¬b }}

• 由蕴含符号 ->> 分隔的一对断言是局部一致的，如果前者蕴含后者：
            {{ P }} ->>
            {{ P' }}
  这对应于 hoare_consequence 的应用, 并且在一段带装饰的程序中， 这是 '唯一' 一个不是完全根据语法机械进行，而是 需要涉及到逻辑和算术推理 来检查装饰正确性的地方。

这些局部一致性条件实质上描述了'验证'给定证明的正确性的过程。 此验证涉及检查每个命令是否与所附断言局部一致。 如果我们对'找到'关于给定规范的证明感兴趣，我们需要发现正确的断言。 除了找到循环不变量比较特殊外，这可以用几乎机械的方式完成。 在本节剩下的内容中，我们将详细解释如何为几个小程序构造装饰， 它们中都没有循环或只有简单的循环不变量。 我们将在下一节中详细讨论如何寻找循环不变量。

示例：使用加法和减法实现交换操作

这是一个运用加法和减法（而不是通过赋值给临时 变量）交换两个变量的值的程序。
       X ::= X + Y;;
       Y ::= X - Y;;
       X ::= X - Y

我们可以使用装饰来 (非形式化地) 证明这个程序是正确的 —— 也就是说，它总是交换变量X和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 }}

这些装饰可以通过以下方式构造:

• 我们以未装饰的程序开始 (即: 所有不带数字编号的行).
• 我们添加规格说明 -- 即: 最外部的前置条件 (1) 和后置条件 (5). 在前置条件中, 我们使用参数 m 和 n 来记住变量 X 和 Y 的初始值, 以便我们可以在后置条件中引用它们.
• 我们机械地从后向前进行, 从 (5) 开始处理直到 (2). 在每一步中, 我们从赋值语句的后置条件获得它的前置条件, 方式是将被赋值的变量替换为赋值语句的右值. 例如, 我们通过替换 (5) 中的 X 为 X - Y 而获得 (4), 然后, 我们通过替换 (4) 中的 Y 为 X - Y 而获得 (3).
• 最终, 我们验证 (1) 逻辑上蕴含 (2) -- 即: 由 (1) 到 (2) 的步骤 是对 '后果法则 (law of consequence)' 的合法运用. 为此我们替换 X 为 m, Y 为 n 并计算如下:
              (m + n) - ((m + n) - n) = n ∧ (m + n) - n = m
              (m + n) - m = n ∧ m = m
              n = n ∧ m = m

请注意, 由于我们在使用 '自然数' 而不是 '定宽的机器整数', 因此我们并不需要担心算术溢出的可能性, 这让事情简单了很多.

Example: Simple Conditionals

这是一个使用了条件语句的简单的带装饰的程序:
      (1) {{True}}
            TEST 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}}
            FI
      (8) {{Z + X = Y ∨ Z + Y = X}}

这些装饰的构造过程如下:

• 我们从最外部的前置条件 (1) 和后置条件 (8) 开始.
• 我们依据 hoare_if 规则所描述的形式, 将后置条件 (8) 拷贝到 (4) 和 (7). 我们合取前置条件 (1) 与分支条件以得到 (2). 我们合取前置条件 (1) 与否定分支条件以得到 (5).
• 为了使用赋值规则得到 (3), 我们替换 (4) 中的 Z 为 Y - X. 为了得到 (6) 我们替换 (7) 中的 Z 为 X - Y.
• 最终, 我们验证 (2) 蕴含 (3) 并且 (5) 蕴含 (6). 这两个蕴含关系都关键地依赖分支条件中提到的 X 和 Y 的顺序. 比如, 如果我们知道 X ≤ Y 那么就能确保在 Y 中 减去 X 再加回 X 仍然得到 Y, 这正是合取式 (3) 的左边. 类似的, 知道 ¬ (X ≤ Y) 能确保在 X 中 减去 Y 再加回 Y 仍然得到 X, 这正是合取式 (6) 的右边. 请注意 n - m + m = n 并 _不是_ 对任意的自然数 n 和 m 总成立的 (比如: 3 - 5 + 5 = 5).

练习：2 星, standard (if_minus_plus_reloaded)

为以下程序填上合法的装饰:
       {{ True }}
      TEST X ≤ Y THEN
          {{ }} ->>
          {{ }}
        Z ::= Y - X
          {{ }}
      ELSE
          {{ }} ->>
          {{ }}
        Y ::= X + Z
          {{ }}
      FI
        {{ Y = X + Z }}

Example: Reduce to Zero

Here is a WHILE loop that is so simple it needs no invariant (i.e., the invariant True will do the job).
        (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). Note that, because the outer postcondition (6) does not syntactically match (5), we need a trivial use of the consequence rule from (5) to (6).
• Assertion (3) is the same as (4), because X does not appear in 4, so the substitution in the assignment rule is trivial.
• Finally, the implication between (2) and (3) is also trivial.

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

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.
       X ::= m;;
       Y ::= 0;;
       WHILE n ≤ X DO
         X ::= X - n;;
         Y ::= Y + 1
       END;

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. 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, 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 (or the induction hypothesis) means that you have a stronger assumption to work with when trying to establish the postcondition of the loop body (or complete the induction step of the proof), but it also means that the loop body's postcondition (or 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. Indeed, 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

练习：2 星, 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.

Exercise: Slow Addition

练习：3 星, 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.

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

练习：3 星, 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. You might find the following lemmas to be useful:

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 is 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 invariant candidate 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

练习：3 星, 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. For full credit, make sure all the arithmetic operations used in the assertions are well-defined on natural numbers.
    {{ X = m }} ->>
    {{ }}
  Y ::= 1;;
    {{ }}
  WHILE ~(X = 0)
  DO {{ }} ->>
       {{ }}
     Y ::= Y × X;;
       {{ }}
     X ::= X - 1
       {{ }}
  END
    {{ }} ->>
    {{ Y = m! }}

Exercise: Min

练习：3 星, standard (Min_Hoare)

Fill in valid decorations for the following program. For the ->> steps in your annotations, you may rely (silently) 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 }}

练习：3 星, 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

练习：4 星, 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.

Weakest Preconditions (Optional)

Some Hoare triples are more interesting than others. For example,
      {{ 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 }}

is useful: 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 triple is still 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 triple (for this command and postcondition) is this one:
      {{ Y ≤ 4 }} X ::= Y + 1 {{ X ≤ 5 }}

In other words, Y ≤ 4 is the weakest valid precondition of the command X ::= Y + 1 for the postcondition X ≤ 5. In general, we say that "P is the weakest precondition of command c for postcondition Q" if {{P}} c {{Q}} and if, whenever P' is an assertion such that {{P'}} c {{Q}}, it is the case that P' st implies P st for all states st.

That is, P is the weakest precondition of c for Q if (a) P is a precondition for Q and c, and (b) P is the weakest (easiest to satisfy) assertion that guarantees that Q will hold after executing c.

练习：1 星, standard, optional (wp)

What are the 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) {{ ? }}
     TEST X = 0 THEN Y ::= Z + 1 ELSE Y ::= W + 2 FI
     {{ Y = 5 }}

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

  6) {{ ? }}
     WHILE true DO X ::= 0 END
     {{ X = 0 }}

练习：3 星, advanced, optional (is_wp_formal)

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

练习：2 星, advanced, optional (hoare_asgn_weakest)

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

练习：2 星, advanced, optional (hoare_havoc_weakest)

Show that your havoc_pre rule from the himp_hoare exercise in the Hoare chapter returns the 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 informal 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 decorate commands as follows:

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

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 special scope called dcom_scope, and we Open this scope for the remainder of the file.