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

How to construct and justify loop invariant, which allows to show partial correctness

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

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

其中|A|是集合A的元素个数,表示q等于集合A的元素个数数组 a 等于 x.

代码 P 指定为:

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

我知道循环不变量一定是真的:

但我不知道我应该如何找到正确的循环不变量,这将使我能够在之后显示 P 的部分正确性。我已经尝试查看循环的每一次迭代和随机 nxa[0.. .n-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 sweep i from 0 to n-1, stopping at n, and at every moment, I keep in q the amount of x that I have found within the array"。循环中涉及的所有变量都必须提到!
  • 将该纯文本翻译成数学,同时确保您的 post 条件反映在不变量中,通常用循环计数器替换 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 扫描的方式不同; 但整体结构相同