如何使用 Hoare 逻辑证明带有 while 循环的程序的正确性？

Question

如何通过 Hoare 逻辑证明具有 while 循环的程序的正确性。有人用任何例子开发它会很有趣，因为我要解决的问题是：

Precondition={n>0}

cont := n;
sum := 0;
while cont <> 0 do:
    sum := sum + cont;
    cont := cont-1;
endwhile

Postcondition={sum=1+2+...+n}

没有必要开发这个例子。我只需要了解程序，因为我没有实际的例子。谢谢你的时间。

Answer 1

霍尔逻辑的"while" rule必须在这里应用：

If a command S satisfies a Hoare triple of the form {P ∧ B} S {P}, then the command while B do S satisfies {P} while B do S {P ∧ ¬B}.

这是证明霍尔逻辑中 while 循环后置条件的唯一技术，因此您必须应用它。代码中给出了条件 B 和循环体 S，但是 P 可以是您选择的任何条件，只要 {P ∧ B} S {P} 成立即可。

这个 Hoare 三元组断言如果 P 在循环迭代之前为真那么它在循环之后仍然为真，所以这样的条件 P 被称为 loop invariant .要证明循环的后置条件，您需要确定 (1) P 在循环的第一次迭代之前为真，以及 (2) P 由循环体保留。

在您的示例中，循环的必要不变量是 sum = n + (n-1) + ... + (cont+1)，即从 cont+1 到 n 的数字之和。一般来说，没有系统的方法来找到合适的循环不变量来使用；你必须利用你对算法的理解，以及你的 intuition/experience 自己想出一个。

---

这足以表明如果循环终止则其后置条件将得到满足；您还需要确定循环 确实 终止。您应该在此处应用的技术是找到 loop variant;这通常是一些整数，(1) 在循环的每次迭代中减少，(2) 当数量达到零时导致循环终止。

在您的示例中，cont 是循环变体，因为循环递减 cont := cont-1，并且循环条件在 cont 达到零时终止循环。一般来说，就像找到一个有用的不变量一样，没有系统的过程可以在所有情况下找到一个变量，但是你可以从查看循环条件开始，看看哪个变量决定了循环何时终止。