language-agnostic - Hoare逻辑循环不变式

Question

我正在查看Hoare Logic，但在理解查找循环不变式的方法时遇到了问题。

有人可以解释用于计算循环不变性的方法吗？

循环不变量应包含什么才能成为“有用”的变量？

我只处理简单的示例，查找不变式，并在示例中证明部分和完整的更正:

{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 }

Answer 1

如果我们谈论的是证明程序的(部分)正确性的Hoare逻辑，则可以使用前提条件和后置条件，分解程序，并使用Hoare Logic推理系统的规则来创建和证明归纳公式。

在您的示例中，您想使用规则分解程序

{p} while b do S {p^not(b)} <=> {p^b} S {p}

在你的情况下

p:i≥0

b:i> 0

S:i:= i-1。

因此，在下一步中，我们推断 {i ≥ 0 ^ i > 0} i := i−1 {i ≥ 0}。可以进一步推断并很容易地证明这一点。
我希望这有帮助。