问题标签 [hoare-logic]

这是算法：

我做了一些研究并将不变量缩小到if x is in a[0 .. n-1] then a[l] <= x < a[r].

我不知道如何从那里取得进展。前提条件似乎太宽泛了，所以我很难证明P -> I.

非常感谢任何帮助。这些是可以用来证明算法正确性的逻辑规则：

假设有一个方法接受两个参数 balance 和 price，它只执行以下操作：

我觉得有两种可能的方法可以用三元组来写这个：

或者

（=> 是暗示）我想知道哪个是正确的？或者两者都是正确的？

我使用 Cormen Algorithms 书中的 Hoare 分区对 Quicksort 进行编码。我无法在我的代码中发现任何错误，它看起来就像书中的伪代码。

完成上述交换后，此代码最终会在 subarray 上进行分区{-3, -2}。为此subarray，pivot is-3和 the partition() returns 0as the index (j)。由于该子数组已经-3在0th index位置处使用枢轴进行排序，因此每次快速排序时都不会进行任何更改。所以 qsort 永远循环。

有人可以告诉我这与书中的 Hoare 分区有何不同，如果相同，为什么这不起作用？

后置条件是：Q = {0 <= x <= 15}

是正确的前提条件 P1 = {-1 <= x} 或 P2 = {0 <= x <= 15}

我该如何计算呢？

我有我的测试代码（用于研究 WP 循环不变量），它在数组单元格中添加了两个长整数，每个数字的表示形式：

我只想指定最后一个循环不变量。我已经用 \at(a[i], LoopCurrent) 尝试了一些 ACSL 代码。我收到未知状态或超时。最后，我完成了一个公理递归解决方案，但没有任何成功。

我现在不知道我还应该尝试什么来验证这一点。帮助？

更新：为实际计算创建了一个函数。改进的公理。仍然有超时状态。使用来自 opam 的 Frama-C 最新版本以默认设置运行（超时 = 10，证明者 Alt-Ergo）。

我有以下示例，我必须证明

使用结果规则我假设 P 是真的

所以从逻辑上讲，Q 应该是真的，但我不确定这是否足够。

试图弄清楚为什么 Hoare 快速排序可以正常工作。基本上我无法向自己证明我们不能创建一个会导致 Hoare 排序算法失败的数组。证明不必是 100% 数学。我只是想相信算法有效。

在下面的代码中，我重写了算法的某些部分以使我更清楚（基本思想保持不变）。

我对该功能100％确定：

1. 函数应该将数组分成两个子数组
   • 低- 包含小于或等于枢轴的元素
   • high - 包含大于或等于枢轴的元素
2. 分区完成后，leftIndex不能大于rightIndex超过 1。换句话说：leftIndex - rightIndex 仅等于 0 或 1。
3. 函数总是返回高子数组中第一个元素的第一个索引

我完全不明白的是：

第一个问题：

为什么如果代码

已经执行，并且在leftIndex等于rightIndex 之后，这并不意味着数组已经成功分区，我们可以返回leftIndex + 1吗？为了澄清我的想法，请看下面的代码：

第二个问题：

让我们想象一下以下场景。假设枢轴值为 10，并且以下代码已成功执行：

之后，假设leftIndex和rightIndex在索引X和value = 6的元素处停止，即arr[X] -> 6。第 3 行将返回索引X + 1的值，比如说8。所以基本上我们会有子数组：

所以高子数组将包含小于枢轴的元素。是否可以创建这样的阵列来复制该场景？

对于最弱的前置条件和最强的后置条件，这是正确的吗？

{P} x = xx; {x'=x}
P: x = 0

{真} y = yy; {Q}
问：y = 0

编辑：

我开始应用它如下：

{true} y = y - y {Q} ==> sp(y = yy; true) = ∃x,y = xx ∧ true

现在我不知道该怎么办；在我看来，“y = 0”最有意义，但这似乎不正确。

我不知道如何找到循环不变量。我不知道从哪里开始。谁能找到给定程序的循环不变量并解释你的方法。

从下面的代码中，我需要推断/选择一个循环不变量。

给出的解决方案是

• s = (x-1)*x/2 ∧ (x ≤ n +1)

我不太明白它是如何达到上述解决方案的。

请帮助我了解如何从代码中得出这样的解决方案或其他循环不变量。