algorithm - 完全正确

Question

[X = M & m >= 0]

y := 0;
z := 0;

while y <> x do
z := z + x;
y:= y +1
end

[z = m x m]

你能帮我解决这个算法的完全正确性吗？

Answer 1

为了证明程序的完全正确，我们需要证明程序的部分正确和终止。

部分正确

|- assert(P); C; assert(Q);

证明部分正确性意味着对于从满足前提条件 P 的状态开始的所有 C 执行，然后在终止时满足后置条件 Q(如果它终止)。

对于您的特定程序，我们正在证明 while 循环的部分正确性，它将具有一个证明结构:

    assert(P);
    assert(Inv);
while B do {
        assert(Inv ^ B);
    C;
        assert(Inv);
};
    assert(Inv ^ !B);
    assert(Q);

其中 Inv 是循环不变式(在每次循环执行之前和之后为真的断言)而 B 是守卫循环的。

终止

要显示 while 循环终止，我们需要找到边界函数。边界函数或变体是一个整数表达式:

• 涉及循环条件的变量
• 必须始终为非负数
• 随着循环的每次迭代而减少

如果边界函数随着每次迭代而减小并且始终为非负值，那么它最终将达到 0，这意味着循环终止。

请试一试。我稍后会发布我的解决方案。

编辑:解决方案

这是我们在填写样板后得到的:

    assert(x==m ^ m>=0);    [Precondition]
y := 0;
z := 0;
    assert(z==y*x ^ x==m);  [Inv]
while y<>x do {
        assert(z==y*x ^ x==m ^ y<>x);    [Inv ^ Guard]
    z := z + x;
    y := y + 1;
        assert(z==y*x ^ x==m);           [Inv]
};
    assert(z==y*x ^ x==m ^ !(y<>x));     [Inv ^ !Guard]

    assert(z==m*m);    [Postcondition]

现在从下往上工作以填补缺失的部分:

    assert(x==m ^ m>=0);    [Precondition]
    assert(0==0*x ^ x==m);  [by arith]
y := 0;
    assert(0==y*x ^ x==m);  [by assignment]
z := 0;
    assert(z==y*x ^ x==m);  [Inv: by assignment]
while y<>x do {
        assert(z==y*x ^ x==m ^ y<>x);    [Inv ^ Guard]
        assert(z+x==y*x+x ^ x==m);       [by arith]
        assert(z+x==(y+1)*x ^ x==m);     [by arith]
    z := z + x;
        assert(z==(y+1)*x ^ x==m);       [by assignment]
    y := y + 1;
        assert(z==y*x ^ x==m);           [Inv: by assignment]
};
    assert(z==y*x ^ x==m ^ !(y<>x));     [Inv ^ !Guard]

    assert(z==m*m);    [Postcondition: by VC1]

VC1 (Verification Condition): z==y*x ^ x==m ^ !(y<>x) |= z==m*m
1) z==y*x ^ x==m ^ !(y<>x)    premise
2) z==y*x ^ x==m ^ y==x       by negation
3) z==y*x ^ x==m ^ y==m       by equality
4) z==m*m                     by equality

边界函数是:x - y