完全正确

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 执行，然后 post条件 Q 在终止时得到满足（如果它终止）。

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

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

其中 Inv 是 循环不变式 （在每次循环执行之前和之后为真的断言）并且 B 是守卫循环。

终止

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

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

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

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

编辑：解决方案

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

    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

完全正确

Total Correctness

algorithm

while-loop

data-structures

部分正确

终止