霍尔逻辑循环不变量答案

【问题标题】：Hoare Logic Loop Invariant霍尔逻辑循环不变量
【发布时间】：2011-06-14 14:19:00
【问题描述】：

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

有人能解释一下用于计算循环不变量的方法吗？

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

我只处理简单的示例，在以下示例中查找不变量并证明部分和完全更正：

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

【问题讨论】：

【解决方案1】：

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

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

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

你的情况

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

【讨论】：

【解决方案2】：

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

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

【讨论】：

对正式事物的非常非正式的解释:)。不变量在开始和结束时不成立，但只要输入满足先决条件，它们就应该在程序的每个语句之后成立。霍尔的逻辑是基于一个简单的程序模式，具体的实现语言并不重要。
嘿，感谢您的评论 :) 在我的教育中，“不变”一词被反复使用，没有正式解释它是什么——我显然提出了一些错误的想法。跨度>
我认为当谈到 Hoare Logic 时，不变量有点乱扔，没有任何好的解释......

【解决方案3】：

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

【讨论】：