问题标签 [hoare-logic]

我正在阅读“带有应用程序的语义 - 正式介绍”一书 - http://www.cs.ru.nl/~herman/onderwijs/semantics2019/wiley.pdf并对此有一些疑问：

1. 在 Ex.2.22, p.39 中，要求表明表 2.2 的结构操作语义是确定性的。是否需要对推导树的形状进行归纳证明，类似于自然语义的证明方式，还是直接按照表2.2中每个规则的定义，证明是确实是确定性的？
2. 在 Ex.6.24, p.190 中，要求显示在 While 语言中添加重复可保持系统完整。我将 [repeat] 的规则定义如下： [repeat]

通过这一点，我希望证明它持有 Q^¬B⇒P（其中 P= wlp（重复 S 直到 b，Q）），并从 [cons] 规则中获得 {P}S{Q} 部分通过证明 wlp(repeat S until b,Q) ⇒wlp(S,Q )，类似于书中证明 [while] 规则在 p.189 中完成的方式。出于某种原因，上述建议似乎对我不起作用。我对 [repeat] 规则的定义是否正确？如果是这样 - 我建议的证明方法是正确的还是我应该尝试不同的方法？

我试图为此代码编写循环不变量和后置条件：

sum = 10是这里明显的后置条件。但是有朋友告诉我，这i = sum也是循环不变量，sum = 12也是后置条件。我检查了以下内容：

• 循环不变量最初是正确的：这是正确的，i = sum因为两者最初都是 0
• 循环不变量被保留：假设i < 10然后i = sum在一次迭代之后它仍然是真的++i = ++sum
• 循环不变量意味着后置条件：假设i >= 10and i = sumthensum = 12也为真

但显然 sum 在这里不等于 12。那么我的推理有什么问题呢？

我目前正在努力弄清楚如何证明包含循环的程序是正确的。我在 wp、vc 和 pc 的基础上工作。

有问题的循环是：

“;”之前的所有内容 是程序和“|”之后的所有内容 是后置条件。

我在讲座中听说你必须找到程序的不变量以及终止函数，但我目前并不知道如何直观地做到这一点。我听说你需要训练这个，但我还没有看到一个例子，主要是理论。如果有人可以帮助我解释循环的验证，那将非常好。

我感谢每一点帮助。

使用霍尔规则我想表明我可以暗示

程序

使用我得到的分配规则

以显示

因此我需要在最后一步显示

我如何证明这一点或我的证明中有什么问题？

我正在阅读这篇研究论文：http ://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.9467&rep=rep1&type=pdf

因此，总而言之，他们正在通过实例化（通过 E 匹配）将量化的 horn 子句转换为无量词的 horn 子句，结果验证条件（VC）在论文的图 6 中给出。

根据我的理解，本文建议将图 6 中生成的 VC 传递给任何 SMT 求解器，因为 VC 现在没有量词并且可以由任何 SMT 求解器求解。（如果我在这方面错了，请纠正我。）

因此，根据这种理解，我尝试使用 z3py 编写图 6 VC。

编辑：我的目标是找到图 6 中 VC 的解决方案。我应该添加什么作为 z3 推断的不变 P 的返回类型？有没有更好的方法使用 z3 来做到这一点？感谢您的时间！

这是代码：

我正在尝试使用 Hoare-Logic 来证明以下 LinearSearch，但我得到了矛盾证明 (1) => (2)。我相信我的不变量应该是不同的。

目前我使用 {s ≥ 0 & s < i → f[s] ≠ value} 作为不变量。这意味着从 0 到 i-1 的所有元素都已经与搜索的值进行了比较，因此从 f[0] 到 f[i-1] 的所有元素都不等于搜索的值。

我开始将规则从算法的底部应用到顶部。

当我试图证明（1）隐含（2）时，矛盾就出现了。因为它在 (1) 中适用于 {f[i] = value} 并且对于所有 s < i 它适用于 f[s] ≠ value。到目前为止这是正确的。

但在 (2) 中，它适用于所有 s <i+1，即 f[s] ≠ 值，因此 f[i] ≠ 值。

矛盾是：证明

我必须证明

这不是真的。

这就是为什么我认为我需要改变我的不变量。但我不知道怎么办？

我正在尝试证明以下 RandomSeach-Algorithm 并找出循环的不变量。

由于该函数randomIndex(..)会创建一个随机数，因此我不能使用像这样的不变量

. 这意味着，0 和 i-1 之间的所有元素，其中 i 是当前检查元素的索引，而不是搜索的元素。

所以我想我定义了一个假设的序列r，其中包含已经与搜索值进行比较或将与搜索值进行比较的所有元素。这就是为什么它只是一个假设的序列，因为在真正比较之前，我实际上不知道将要与搜索值进行比较的元素。

这意味着它适用r.lenght() ≤ runs 并且在找到搜索元素的情况下

然后我可以定义一个不变量，如：

我可以这样做吗，因为序列 r 不是真实的？感觉不对。有人对不变量有不同的想法吗？

该程序：

我不确定x这个 Hoare 三元组中的值：{ a = 0 } while (x > a) do (x := x − 1) { x = 0 }.

对于如何证明这个 Hoare 三元组是否有效，我有 2 个潜在的想法：

• 假设x为 0，Hoare 三元组有效，或
• 假设x是任意值，我们将其分解为案例并得出结论，Hoare 三元组并非对所有值都有效x

上述任何一种方法是否有效，还是我应该采取另一种方法？