问题标签 [hoare-logic]

证明以下是正确的。

以下推理规则应该会有所帮助

我一直在网上寻找一个清晰的解释或至少一个示例，但我不太明白，我在下面找到了一些可能有帮助的网站，但没有任何示例。

第 148-160 页

非常感谢任何帮助，我希望看到这个问题完成，以便我可以做其他人，我非常卡住，这本书没有显示任何示例。

这些链接也可能有一些帮助。谢谢，10分！

http://en.wikipedia.org/wiki/Hoare_logic#Conditional_rule

给定一个循环不变量，维基百科列出了一个为循环生成最弱前提条件的好方法（来自http://en.wikipedia.org/wiki/Predicate_transformer_semantics）：

M[x <- N] 用 N 替换 M 中所有出现的 x。

现在，我的问题是变量 y。\forall y, 在表达式中绑定 y，因此“y 是新变量的元组”不会为我解析。\forall 中的 y 是否与 "[x <- y]" 中的 y 相同？我根本无法解析上述内容。

编辑：改写以避免参考请求。

我的问题是：循环不变量和计算最弱前提（如果有的话）之间的直接联系是什么。似乎在实践中所做的很多事情都将循环的最弱前提条件放松为适合验证的前提条件。来自维基百科的上述内容表明，给定一个循环不变量，确实可以计算出鼻子上最弱的先决条件，但我无法理解这个条件。

在 cormen 中给出的 Hoare 分区：

在快速排序中使用它时，以 {1,3,9,8,2,7,5} 作为输入，在第一个分区获得 {1,3,5,2,8,7,9} 之后，这是不正确的因为，所有小于枢轴的元素（这里是 5 ）都应该在左侧。有人可以指出我缺少什么吗？

在使用 Hoare Logic 之前，我们如何重复证明一个程序？

我发现了这样的规则：

对于 {P} 重复 S 直到 B {Q}

但我仍然找不到任何解释如何使用此规则

例如在这个问题中：

我如何使用该规则来证明这个程序？

我正在学习 Z3，并希望输入一些 Hoare 逻辑所述的验证条件，并获得给定 Hoare 三元组的模型。

到目前为止，我只能验证分配，这是一个示例（只是为了检查我是否做对了）：

Given: { x< 40 } x :=x+10 { x < 50}

但我不知道如何验证 If-Else，例如：

{0 ≤ x ≤ 15 } if x < 15 then x := x + 1 else x := 0 endif {0 ≤ x ≤ 15 }

或 While 循环（部分正确性）

{x ≤ 10} while x < 10 do x := x + 1 done {¬x < 10 ∧ x ≤ 10}

我尝试使用 if-else 的 ite 命令，但它似乎不受支持。

希望你能帮我解决这个问题。

我有一个程序，我应该在其中找到一个循环不变量，然后提供一个证明。

对我来说唯一的逻辑循环不变量是res<=x*y，这从后置条件很简单，但我认为它不是最好的。也许还有其他建议？

我有以下问题：前提条件为真

我正在考虑的变体是：n-i. 但是，我认为没有任何东西可以阻止用户提供负值，在这种情况下，变体将为负值（这与其定义相矛盾）。

是否可以将不变量指定为 |n| -i，还是必须将 n>=0 作为前提条件？

任何帮助或建议将不胜感激。

我是逻辑世界的新手。我正在学习 Hoare Logic 和程序的部分和全部正确性。我尝试了很多解决以下问题但失败了。

我的一位朋友给了我以下答案，但我不知道它是否正确。

请一步一步教我如何解决这个问题。

除了下面，还有没有更好的方法来使用随机枢轴进行快速排序（我不能没有交换）？请指教

另外，如果不正确，请告诉我。谢谢！

我正在尝试编写自己的 hoare 分区函数以更好地理解它。我以为我很好地遵循了它的定义和伪代码，但即使它在很多情况下似乎都按预期工作，但当传入多个值等于 pivot 的列表时，它会崩溃并进入无限循环。我的错误在哪里，我应该如何修改它以修复错误？