algorithm - 如何构造和证明循环不变量，这允许显示部分正确性

Question

我需要构造并证明一个具有给定规范的循环不变量:

{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] 查看在循环运行时哪些值的组合是恒定的，但这没有帮助。

Answer 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

解决这些问题时，你可以尝试这两个步骤:

• 尝试用纯文本描述算法中发生的事情:“我将 i 从 0 扫描到 n-1，在 n 处停止，并且在每时每刻，我都在 q 中保留 x 的数量。我在阵列中找到的”。必须提及循环中涉及的所有变量!
• 将该纯文本翻译成数学，同时确保您的后置条件反射(reflect)在不变量中，通常替换 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 注意不同的限制，反射(reflect)出 i扫地方式不同； 但整体结构相同