language-agnostic - 霍尔逻辑循环不变量

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}

在你的情况下

• p: i≥0
• b: 我 > 0
• S: i := i-1。

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

Answer 2

我不确定这是否会回答您的问题，但以防万一：

• “循环不变量”非正式地是在循环迭代之前和之后保持正确的事实陈述。它本质上定义了程序相对于该循环的一致性约束。
• 我对 Hoare Logic 的了解还不够，无法准确地告诉您如何“计算”循环不变量，但我怀疑这样的事情将更多地取决于被分析的代码的语言，而不是形式证明语言本身。您是否有正在使用的正式算法描述？如果有更多的背景知识，我可能会走得更远。
• 有用的循环不变量将描述有关应用程序状态的特定内容。例如，如果您正在编写插入排序，主元素运动循环的一个有用的循环不变量将基本上说明（子）列表在循环执行之前和之后包含相同的对象集合，并且可能之前的元素in sorted order 保持排序顺序。

Answer 3

有用（出于您的推理）是不变量的要点。因此，请查看您要证明的后置条件并尝试构建一个不变量，该不变量将帮助您逐步达到后置条件，并且可以从循环代码中导出。