GCD 部分正确性证明（用到循环不变式）

发表于 更新于 分类于 阅读次数：

本文详细的讲解了一些证明程序正确性的概念，并以一个例子详细介绍了如何用循环不变式证明程序的部分正确性。

概念包括：

  • 前置断言、后置断言
  • 循环不变式
  • 程序的正确性 （部分正确性、完全正确性）

概念解读

前置断言（pre-condition）

程序执行前的输入应满足的条件，又称为输入断言。

后置断言（post-condition）

程序执行后的输出应满足的条件，又称为输出断言。

程序规约

对程序所实现功能的精确描述，由程序的前置断言和后置断言两部分组成。

程序规约Q{S}R 是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为 “程序S，关于前置断言Q和后置断言R是完全正确的”。

正确性

部分正确

若对于每个使得Q(i)为真、且使得程序S计算终止的输入信息i，R(i,S(i))都为真，则称程序S关于Q和R是部分正确的。
​

程序终止

若对于每个使得Q(i)为真的输入i，程序S的计算都终止，则称程序S关于Q是终止的。
​

完全正确

程序是部分正确，同时又是终止的。

在书写程序规约时，使用Q表示前置断言，R表示后置断言，S表示问题求解的实现程序。在前置断言Q之前，还必须给出Q和R中所出现的标识符的必要说明。

循环不变式

  • 初始化：在循环的第一轮迭代前是正确的；
  • 保持：如果在循环的某一次迭代开始之前是正确的，那么在下一次迭代开始之前，也是正确的；
  • 终止：当循环结束，不变式给了我们一个有用的性质。

当前两个性质成立时，就能保证循环不变式在循环的每一轮迭代开始之前，都是正确的。第三项“终止”是最重要的，因为我们是用不变式来证明算法的正确性。

证明GCD的部分正确性

背景

GCD（greatest common divisor）程序是用来计算两个正整数的最大公约数。

原gcd程序如下：

1
2
3
4
5
6
7
gcd(X,Y):
    A := X; B := Y;
    while A ≠ B do
    begin
        while A > B do A := A–B;
        while B > A do B := B–A
    end

三条公理

证明过程中，我们会用到如下三条公理：

  • $X>Y ⇒ GCD(X,Y) = GCD(X–Y,Y)$

  • $GCD(X,Y) = GCD(Y,X)$

  • $GCD(X,X) = X$

加上循环不变式P之后：(只分析程序内部)

1
2
3
4
5
6
7
8
9
10
11
12
13
{ X > 0 ∧ Y > 0 }  -- 因为X，Y为两个正整数

A := X; B := Y;

{ P }

while A ≠ B do
begin
	while A > B do A := A–B;
	while B > A do B := B–A
end

{ A = GCD(X,Y) }  -- 最后要求出X，Y的最大公约数。

设P为$GCD(X,Y) = GCD(A,B) ∧ A > 0 ∧ B > 0$. 下面，我们一步步来证明这个循环不变式在整个程序循环过程中都始终满足。

步骤一

1
2
3
{ X > 0 ∧ Y > 0 }
A := X; B := Y;
{ P }

证明“当前置断言{ X > 0 ∧ Y > 0 } 满足且执行完赋值语句之后，后置断言能满足P”

因为A，B分别被赋值为X，Y，而前置断言 $X>0\wedge Y>0$, 所以可以得出 $A > 0 \wedge B> 0 $ ；且由于赋值，所以$GCD(A,B) = GCD(X,Y)$. 所以满足P。

接下去，因为这个GCD程序还包含两个内部循环，所以我们仍然需要为它们构建循环不变式。幸运的是，这两个内部循环的循环不变式与外部的循环不变式P是相同的。接下来的两个步骤我们将分别证明它们。

步骤二

先看第一个内部循环：

1
2
3
{ P }
while A > B do A := A–B;
{ P }

把$A>B$ 放入前置断言中，则有：

1
2
3
{ P ∧  A > B}
 A := A–B;
{ P[A → A–B] }

要证明“如果前置断言{ P ∧ A > B}满足，则执行了语句之后，后置断言也满足”。所以我们先假设前置断言已经满足了，可以执行这个语句，A被赋值为A-B，那么现在就要证明后置断言也满足。

可以看到，后置断言中的A被替换成了A-B：

$$P[A \rightarrow A-B] \equiv GCD(X,Y) = GCD(A-B,B) ∧ A-B > 0 ∧ B > 0 $$

再推一步：

$P[A \rightarrow A-B] \equiv GCD(X,Y) = GCD(A-B,B) ∧ A > B ∧ B > 0$ .

也就等于前置断言$P \wedge A > B$。所以当前置断言满足时，后置断言也满足；又因为$P \wedge A > B$ 可以弱化为P，所以前置断言及后置断言都可以满足P。所以对于这一个内部循环，P是它的循环不变式。

步骤三

第二个内部循环的证明过程与第一个内部循环一样，证明过程相同。

1
2
3
{ P }
while A < B do B := B–A;
{ P }

可得：

1
2
3
{ P ∧  B > A}
 B := B–A;
{ P[B → B–A] }

证明过程如步骤二。

步骤四

1
2
3
4
5
6
{ P }
begin
	while A > B do A := A–B;
	while B > A do B := B–A
end
{ P }

要证明“执行完这两个内部程序之后，循环不变式P依然成立”。这个证明可以由步骤二和三给出：如果执行的是第一个内部循环，则后置断言可以满足P；如果执行的是第二个内部循环，后置断言依然可以满足P。也就是说，无论执行的是哪个循环，P都是它们的循环不变式，因此都可以保证当前置断言P被满足时，执行完循环语句后，后置断言依然会满足P。

步骤五

1
2
3
4
5
6
7
{ P }
while A ≠ B do
begin
	while A > B do A := A–B;
	while B > A do B := B–A
end
{ P ∧ A=B }

要证明 “如果满足前置断言P，且执行了while A ≠ B 的循环体之后，后置断言满足{P ∧ A=B }”。

这个是显然的，因为循环结束的条件是A ≠ B，所以结束时一定满足A = B。 而之所以满足P，是因为步骤四已经证明两个内部循环结束后，P仍然满足。

步骤六

将步骤五的后置断言进行推导：

$$P ∧ A=B ≡ (GCD(X,Y) = GCD(A,B) ∧ A > 0 ∧ B > 0 ∧ A=B) $$

由公理 $GCD(X,X) = X $ 可知 $GCD(A,A) = A$. 所以可结合$A = B$推出 $GCD(X,Y) = A$。

所以可以得出，最外层的while执行完后，既满足P，也满足原来的后置断言{$GCD(X,Y) = A$}.

步骤七

结合步骤一（while循环前）和步骤六（while循环），证明完毕。