完全正确答案

【问题标题】：Total Correctness完全正确
【发布时间】：2015-04-17 23:00:56
【问题描述】：

[X = M & m >= 0]

y := 0;
z := 0;

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

[z = m x m]

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

【问题讨论】：

完全正确是什么意思？
你是在问算法是否正确？如果是这样，是的。 y 以1 为步长增加到m，z 以m 为步长增加到m*m。
你能把符号给我吗？
谷歌搜索了一下，看起来“完全正确”的意思是“给定前提条件（第一组方括号中的东西）和源代码，证明源代码最终终止，并且当它发生时，后置条件（第二组方括号中的东西）总是成立的。”
@yusuf，“你能帮我解决[问题]吗？”抱歉，这个问题对 SO 来说有点太宽泛了。您还有什么比“我该怎么做？”更具体的问题吗？

标签： algorithm data-structures while-loop

【解决方案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

【讨论】：