Hoare Logic Loop Invariant

Question

我正在研究Hoare Logic,我在理解寻找循环不变量的方法时遇到了问题.

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

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

我只是处理简单的例子,找到不变量并在例子中证明部分和完全的纠正:

{ i ? 0 } while i > 0 do i := i?1 { i = 0 }

Answer 1

如果我们谈论的是用于证明程序（部分）正确性的霍尔逻辑，那么您使用前置条件和后置条件，分解程序并使用霍尔逻辑推理系统的规则来创建和证明归纳公式。

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

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

在你的情况下

• 丙：我？0
• b: i > 0
• S: i := i?1。

所以在下一步中我们推断{i ? 0 ^ i > 0} i := i?1 {i ? 0}。这可以很容易地进一步推断和证明。我希望这有帮助。