1

我需要用给定的规范构造和证明一个循环不变量：

{n > 0} P {q = | {j: a[j]=x and 0 <= j < n} |}

其中|A| 是集合 A 的元素数。这意味着q等于数组a中等于x的元素数。

代码P指定为：

{
int i = 0, q = 0;
while (i != n){
    if (a[i] == x)
        q = q + 1;
    i = i + 1;
}

我知道循环不变量必须是真的：

  • 在循环开始之前
  • 在循环的每次迭代之前
  • 循环结束后

但我不知道如何找到正确的循环不变量，这将允许我在之后显示 P 的部分正确性。我已经尝试查看循环的每一次迭代以及随机n、x和a[0...n-1] 的变量，以查看在循环工作时哪些组合的值是恒定的，但这没有帮助。

4

1 回答 1

1

仔细查看您的代码。一开始，q是 0，只有当你找到新的元素时它才会增长== x。所以

q = | {j: a[j]=x and 0 <= j < i} |

是你的不变量的一部分。请注意，在您的规范中，您< n使用的是< i. 还要注意，在循环终止时，i == n. 所以它在开始时也是有效的。在两者之间的任何时候也是如此：到目前为止，非常好。还缺少什么吗？是的，我们还应该声明

0 <= i <= n-- 因为它描述了 i 的值的范围（否则，i可以自由地在数组之外冒险）。

这就是全部吗？是的——没有其他循环状态可以描述。因此，您的完整不变量看起来像

q = | {j: a[j]=x and 0 <= j < i} | and 0 <= i <= n

解决这些练习时，您可以尝试以下 2 个步骤：

  • 尝试用纯文本描述算法中发生的事情：“我i从 0 扫描到 n-1，在 n 处停止，并且每时每刻，我都保持在数组中找到q的数量”。x必须提及循环中涉及的所有变量！
  • 将该纯文本转换为数学，同时确保您的后置条件反映在不变量中，通常用n循环计数器替换（在这种情况下，i）

作为一个思想实验，尝试用等效循环编写不变量（但从结尾迭代到开头）：

{
int i = n-1, q = 0;
while (i >= 0){
    if (a[i] == x)
        q = q + 1;
    i = i - 1;
}

将鼠标悬停在答案上（但请先尝试弄清楚）。

q = | {j: a[j]=x and i < j < n} | and -1 <= i < n 注意不同的限制，反映不同的i扫描方式；但整体结构相同

于 2018-12-12T09:24:48.750 回答