如何使用Hoare逻辑在一段时间内演示程序的正确性？

Question

我如何通过Hoare逻辑证明一个有一段时间周期的程序的正确性。令人着迷的是有人用任何示例进行了开发，因为我要解决的问题是：

前提条件= {n> 0}

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

后置条件= {sum = 1 + 2 + ... + n}

没有必要开发此示例。我只需要了解该过程，因为我没有一个实际的例子。感谢您的宝贵时间。

Answer 1

必须在此处应用Hoare逻辑的"while" rule：

如果命令S满足形式为{P ∧ B} S {P}的Hoare三元组，则命令while B do S满足{P} while B do S {P ∧ ¬B}。

这是在Hoare逻辑中证明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的数字之和。通常，没有系统的方法来找到要使用的正确循环。您必须使用对算法的理解以及您的直觉/经验来提出自己的想法。

---

这足以表明if循环终止，则将满足其后置条件；您还需要确定循环does终止。您应该在此处应用的技术是找到一个loop variant。这通常是一些整数，该数量（1）在循环的每次迭代中都会减少，并且（2）在该数量达到零时使循环终止。

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