Floyd不变式断言法在

1、带你走进带你走进WYQWYQ的世界的世界1.Floyd1.Floyd不变式断言法不变式断言法不变式断言法是Floyd提出的，它是程序正确性证明的基本方法。利用不变式断言法证明一个程序的部分正确性部分正确性时，通常分为三个步骤！2.举例说明FLOYD不变式断言法举例求解：两个非零整数x, y( x, y不能同时为零)的最大公约数。这个算法很多同学都无法真正理解，为何一个如此简短的循环可以求出任意两个非负整数的最大公约数。#includemain() int x, y , s ;scanf(%d%d,&x,&y);while(x!=0)if (y=x) y=y-x;else s=x

2、; x=y; y=s; printf(%d,y);1.1.建立断言，假定建立断言，假定x,yx,y的初始值为的初始值为x0,y0,x0,y0,可以建立下面的输入，输可以建立下面的输入，输出断言和不变式断言。出断言和不变式断言。输入断输入断言：言：x0=0 x0=0y0=0y0=0(x00Vy00)(x00Vy00)输出断输出断言：言：y=GCD(x0,y0)y=GCD(x0,y0)不变式断不变式断言：言：x=0 x=0y0=0y0=0(x00Vy00)(x00Vy00)GCD(x,y)=GCD(x0,y0)GCD(x,y)=GCD(x0,y0)可以将这些断言直接写入程序的适当位置，即可将程序写

3、为：可以将这些断言直接写入程序的适当位置，即可将程序写为：A A：scanf (“%d%d”,&X,&y);scanf (“%d%d”,&X,&y); x0=0 x0=0y0=0y0=0(x00Vy00)(x00Vy00)L L：while (x!=0)while (x!=0)x=0 x=0y=0y=0(x0Vy0)(x0Vy0)GCD(x,y)=GCD(x0,y0)GCD(x,y)=GCD(x0,y0)B: if (y=x) y=y-x;B: if (y=x) y=y-x;C: else s=x;x=y;y=s;C: else s=x;x=y;y=s;D:pr

4、intf (“%d”,y);D:printf (“%d”,y);y=GCD(x0,y0)y=GCD(x0,y0).022.2.建立检验条件建立检验条件程序执行中所有可能的通路可以分解为以下四条通路：程序执行中所有可能的通路可以分解为以下四条通路：通路一：通路一：ALAL；通路二：通路二：LBLLBL；通道三：通道三：LCLLCL；通道四：通道四：LD;LD; GCDGCD（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，），（，），?最大公约数的基本定理最大公约数的基本定理对于通道一的检验条件1: x0=0 x0=0y0=0y0=0(x00Vy00)(x0

5、0Vy00)x=0 x=0y=0y=0(x0Vy0)(x0Vy0)GCD(x,y)=GCD(x0,y0)GCD(x,y)=GCD(x0,y0)A L 对于通道二的检验条件2: L B L x=0y=0(x0Vy0)GCD(x,y)=GCD(x0,y0)x0y=x x0=0y-x=0(x0Vy-x0)GCD（x,y-x=0）GCD(x, y-x)=GCD(x0,y0)对应于通路三的检验条件3: L C Lx=0y=0(x0Vy0)GCD（，）GCD(x0,y0)x0y=0 x=0(y0Vx0)GCD(y,x)=GCD(x0,y0)对应于通路四的检验条件4: L Dx=0y=0(x0Vy0)GCD

6、(x,y)=GCD(x0,y0) y=GCD(x0,y0）3.3.证明检验条件证明检验条件假假定输入断言成立，若能证明四个检验条定输入断言成立，若能证明四个检验条件成立，则程序部分正确的。件成立，则程序部分正确的。证证明检验条件明检验条件1:1:由于这时由于这时x,yx,y的值为初始的值为初始值值x0,y0,x0,y0,因而检验条件因而检验条件1 1可以改写成如下可以改写成如下形式：形式：x0=0 x0=0y0=0(x00Vy00) x0=0 x0=0y=0(x00Vy00)GCD(x0,y0)=GCD(x0,y0),此藴涵式显然成立。于是此藴涵式显然成立。于是检验一为真。检验一为真。证明检验

7、证明检验2:2:对于检测条件对于检测条件2 2，若藴涵式前项成若藴涵式前项成立，即立，即x=0,y=xx=0,y=x为真，从而为真，从而x=0,y-x=0 x=0,y-x=0为为真，又已知真，又已知x0 x0为真，从而为真，从而为真。为真。另外，根据数论知识，当另外，根据数论知识，当y=xy=x时有时有GCDGCD（，）（）（，），），又根据藴涵式又根据藴涵式前项前项GCDGCD（，）（）（，）为真，从而为真，从而GCDGCD（，）（，）（，），）为真，于是，检验条件为真。为真，于是，检验条件为真。证明检验条件：证明检验条件： 根据数论知识，根据数论知识， GCDGCD（y,xy,x）=GCD(x,y),=GCD(x,y),又根据藴涵式前项又根据藴涵式前项GCD(x,y)=GCD(x0,y0)GCD(x,y)=GCD(x0,y0)为真，从而为真，从而GCDGCD（y,xy,x）=GCD(x0,y0)=GCD(x0,y0)为真。于为真。于是，检验条件是，检验条件3 3为真。为真。证明检验条件证明检验条件4 4： 由藴涵式前项由藴涵式前项x=0 x=0y=0(x0