问题标签 [hoare-logic]

我不确定

是一个有效的Hoare 三元组。

我不确定是否允许引用变量（在本例中为y），而无需先在三重程序主体或前置条件中明确定义它。

如何？

我正在研究一些 Hoare 逻辑，我想知道我的方法是否正确。

我有以下程序P：

它应该满足 hoare 三元组 {n >= 0}P{s = n*(n+1)/2} （所以它只需要总和）。现在，最初我有 |s = i*(i-1)/2| 作为我的不变量，效果很好。但是，从循环结束到我想要的后置条件，我遇到了问题。因为为了暗示

要持有，我需要证明 i 是 n+1，而不仅仅是任何大于 n 的 i。所以我想到的是在不变量中添加一个 (i <= n + 1) ，这样它就变成了：

然后我可以证明这个程序，所以我认为它应该是正确的。

尽管如此，我发现不变量有点“不变”:)。不像我在课程或练习中看到的任何东西，所以我想知道这里是否有更优雅的解决方案？

我想知道是否有人可以帮助我回答这个问题。它来自以前的试卷，我可以知道为今年考试准备的答案。

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？

考虑以下涉及整数变量的代码部分：

通过陈述一个合适的输出条件，然后验证这段代码的正确性，证明执行后m等于i和j的最小值。

我的后置条件为：{m = i ∧ i < j ∨ m = j ∧ j < i}

它是否正确？你如何验证这一点？

我正在尝试编写一个 Hoare 分区函数，该函数将数组作为输入，并将第一个元素作为枢轴进行分区（我知道这不是一个好主意，我应该使用随机枢轴，就像这种median-of-medians方法一样）。问题是当第一个元素最高时，这个函数会陷入无限循环，就像数组一样[14,6,8,1,4,9,2,1,7,10,5]。我可以看到错误，在外部的第一次迭代之后while，两者都i等于j10，因此循环永远继续。我应该修补哪个部分以获得预期的效果？这是代码：

根据许多网站给出的伪代码，我编写了这个Hoare分区算法，它采用一个数组，子数组的开始和结束索引根据给定的枢轴进行分区。它工作正常，但有人可以解释逻辑，它是如何做的吗？这里的代码：

分区还有另一种变体，即Lomuto算法。它做了类似的事情，虽然因为我一开始不理解Hoare算法，所以我看不出区别。任何人都可以解释算法中发生了什么，以及在哪种情况下哪个提供更好的性能？

这是一个核心问题 ，请不要说关于语法或语义，问题是两者之间的实际区别是什么

WHILE循环和FOR循环，for循环中编写的所有内容都可以用while循环完成，那么为什么要两个循环呢？

这是在剑桥大学的一次研讨会上提出的。所以我认为我们必须在性能开销和 WC 复杂性方面进行解释。

我认为我们必须按照弗洛伊德霍尔的逻辑

我正在推理 Hoare Logic 的练习。

我应该找到满足三元组的所有布尔表达式B和所有程序S，假设 的评估不能修改存储，但执行可以修改它并改变 的值。P{true} if B then S; if B then P; {a >= 0}BSB

特别是，我不知道我能说什么a，因为它只存在于后置条件中，我从未找到过这样的例子。

谢谢你的帮助！

我正在教授一门关于 FOL 和程序验证的课程，灵感来自 Mordechai Ben-Ari，计算机科学的数学逻辑，Springer，1993-2012 年。我想通过让学生使用 Python 编程来说明概念。

对于 FOL，我使用的是 NLTK，它具有出色的 FOL 包。

但是我还没有找到用于程序验证的Python包：插入前置条件和后置条件逻辑公式，查找循环不变量，逐步验证Python程序等。换句话说，在Python中使用Hoare逻辑框架并用于Python程式。

你知道这个任务的任何包吗？

我想知道是否有人可以帮助我回答这个问题。它来自以前的试卷，我可以知道为今年考试准备的答案。

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？以下算法找到最大值是否正确？

答案必须基于算法最弱前提的计算。

你如何验证这一点？似乎很简单。

谢谢。

我们可以在 z3 中设计关于分离逻辑的推理规则和公理，并用它来自动证明一些 props 吗？例如，“x=y /\ (x |-> z) |- x=y /\ (y |-> z)”