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

Question

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

前提条件={n>0}

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

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

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

score 3 · Accepted Answer

霍尔逻辑的“while”规则必须在这里应用：

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

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

这个 Hoare 三元组断言如果P在循环迭代之前为真，那么之后它仍然为真，因此这种条件P称为循环不变量。要证明循环的后置条件，您需要在循环P的第一次迭代之前建立 (1) 为真，以及 (2)P由循环体保留。

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

这足以表明如果循环终止，那么它的后置条件将被满足；您还需要确定循环确实终止。您应该在这里应用的技术是找到一个循环变体；这通常是某个整数量，它 (1) 在循环的每次迭代中都会减少，并且 (2) 当数量达到零时会导致循环终止。

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

1 回答 1