隐式迁移模型中国科学院软件研究所张文辉http:/lcs.ios.ac.cn/zwh/pv2结构化循环语句模型i:=1; j:=0; k:=0; l:=1; while (x=y) do if xy then x:=x-y; i:=i-k; j:=j-1; else y:=y-x; k:=k-i; l:=l-j; fi od 3结构化循环语句模型：例子4结构化循环语句模型：示意图i:=1(x=y) xyendyesnoyesnoj:=0k:=0l:=1x:=x-yi:=i-kj:=j-1beginy:=y-xk:=k-il:=l-jwhile (x=y) do if xy then x:=x-y; else y:=y-x; fi od 5结构化循环语句模型：例子6结构化循环语句模型：示意图(x=y) xyendyesnoyesnox:=x-ybeginy:=y-xB=(F,P)和V:F = -P = =,V = x,yI=(Int,I0)I0(-) =- I0(=) = = I0() = 7结构化循环语句模型：F,P,VS0: while (x=y) do odS1: if xy then x:=x-y; else y:=y-x; S0S2: x:=x-y; S0S3: y:=y-x; S0S4: 8结构化循环语句模型：相关模型变量状态集合: = (x,y) | x,y 为整数 系统状态集合: S0,S1,S2,S3,S4 初始状态集合: S0 9结构化循环语句模型：状态S0,(4,6)S1,(4,6)S3,(4,6)S0,(4,2)S1,(4,2)S2,(4,2)S0,(2,2)S4,(2,2)10结构化循环语句模型：运行例子while (x=y) do odif xy then x:=x-y; else y:=y-x; S0y:=y-x; S0while (x=y) do odif xy then x:=x-y; else y:=y-x; S0x:=x-y; S0while (x=y) do od11结构化循环语句模型：性质(x=y) xyendyesnoyesnox:=x-ybeginy:=y-xx=a, y=b,a0, b0y=gcd(a,b)12流程图模型beg: (i,j,k,l):=(1,0,0,1) goto l1l1:if (x=y) goto l2 else goto endl2:if (xy) goto l3 else goto l4l3: (x,i,j):=(x-y,i-k,j-l) goto l1l4: (y,k,l):=(y-x,k-i,l-j) goto l113流程图模型：例子14流程图模型：示意图l1(y,k,l):=(y-x,k-i,l-j)(x,i,j):=(x-y,i-k,j-l)l2beg(i,j,k,l):=(1,0,0,1)(x=y) xyendl4l3yesnoyesnobeg: if (x=y) goto l2 else goto endl2:if (xy) goto l3 else goto l4l3: (x):=(x-y) goto begl4: (y):=(y-x) goto beg15流程图模型：例子16流程图模型：示意图beg(y):=(y-x)(x):=(x-y)l2(x=y) xyendl4l3yesnoyesnoB=(F,P)和V:F = -P = =,V = x,yI=(Int,I0)I0(-) =- I0(=) = = I0() = 17流程图模型： F,P,Vbeg: if (x=y) goto l2 else goto endl2:if (xy) goto l3 else goto l4l3: (x):=(x-y) goto begl4: (y):=(y-x) goto begend:18流程图模型：标号变量状态集合: = (x,y) | x,y 为整数 系统状态集合: beg,l2,l3,l4,end 初始状态集合: beg 19流程图模型：状态beg,(4,6)l2,(4,6)l4,(4,6)beg,(4,2)l2,(4,2)l3,(4,2)beg,(2,2)end,(2,2)20流程图模型：运行例子if (x=y) goto l2 else goto endif (xy) goto l3 else goto l4(x):=(x-y) goto begif (x=y) goto l2 else goto endif (xy) goto l3 else goto l4(y):=(y-x) goto begif (x=y) goto l2 else goto end21流程图模型：性质beg(y):=(y-x)(x):=(x-y)l2(x=y) xyendl4l3yesnoyesnox=a, y=b,a0, b0y=gcd(a,b)22卫式迁移模型(a=s0) (i,j,k,l,a):=(1,0,0,1,s1)(a=s1 x=y) (a):=(s5)(a=s1 (x=y) (a):=(s2)(a=s2 xy) (a):=(s3)(a=s2 (xy) (a):=(s4) (a=s3) (x,i,j,a):=(x-y,i-k,j-l,s1) (a=s4) (y,k,l,a):=(y-x,k-i,l-j,s1)初始状态： (a=s0x0y0)23卫式迁移模型：例子24卫式迁移模型：示意图(a=s0) (i,j,k,l,a):=(1,0,0,1,s1)(a=s1x=y) (a):=(s5)(a=s1(x=y) (a):=(s2)(a=s2xy) (a):=(s3)(a=s2(xy) (a):=(s4) (a=s3)(x,i,j,a):=(x-y,i-k,j-l,s1) (a=s4)(y,k,l,a):=(y-x,k-i,l-j,s1)初始状态: a=s0x0y025卫式迁移模型：示意图s5s0(a=s0) (i,j,k,l,a):=(1,0,0,1,s1)(a=s1x=y) (a):=(s5)(a=s1(x=y) (a):=(s2)(a=s2xy) (a):=(s3)(a=s2(xy) (a):=(s4) (a=s3)(x,i,j,a):=(x-y,i-k,j-l,s1) (a=s4)(y,k,l,a):=(y-x,k-i,l-j,s1)s1s2s3s4初始状态: a=s0x0y0(a=s1 x=y) (a):=(s5)(a=s1 (x=y) (a):=(s2)(a=s2 xy) (a):=(s3)(a=s2 (xy) (a):=(s4) (a=s3) (x,a):=(x-y,s1) (a=s4) (y,a):=(y-x,s1)初始状态： (a=s1x0y0)26卫式迁移模型：例子27卫式迁移模型：示意图(a=s1x=y) (a):=(s5)(a=s1(x=y) (a):=(s2)(a=s2xy) (a):=(s3)(a=s2(xy) (a):=(s4) (a=s3)(x,a):=(x-y,s1) (a=s4)(y,a):=(y-x,s1)初始状态: a=s1x0y0B=(F,P)和V:F = s1,s2,s3,s4,s5,-P = =,V = a,x,yI=(Int,I0)I0(si) =i for i 1,2,3,4,5I0(-) =- I0(=) = = I0() = 28卫式迁移模型： F,P,V变量状态集合: = (a,x,y) | a,x,y 为整数 初始状态集合: (1,x,y) | x,y 为自然数 29卫式迁移模型：状态(s1,4,6)(s2,4,6)(s4,4,6)(s1,4,2)(s2,4,2)(s3,4,2)(s1,2,2)(s5,2,2)30卫式迁移模型：运行例子31卫式迁移模型：性质(a=s1x=y) (a):=(s5)(a=s1(x=y) (a):=(s2)(a=s2xy) (a):=(s3)(a=s2(xy) (a):=(s4) (a=s3)(x,a):=(x-y,s1) (a=s4)(y,a):=(y-x,s1)(a=s5 y=gcd(m,n)(a=s5 y=gcd(m,n)初始状态: a=s1x0y0 (x=my=n) 32谓词迁移模型迁移关系： (a=s0a=s1i=1j=0k=0l=1x=xy=y) (a=s1x=ya=s5i=ij=jk=kl=lx=xy=y) (a=s1(x=y)a=s2 i=ij=jk=kl=lx=xy=y) (a=s2xya=s3i=ij=jk=kl=lx=xy=y) (a=s2(xy)a=s4i=ij=jk=kl=lx=xy=y) (a=s3a=s1i=i-kj=j-lk=kl=lx=x-yy=y) (a=s4a=s1i=ij=jk=k-il=l-jx=xy=y-x) 初始状态：(a=s0x0y0)33谓词迁移模型：例子34谓词迁移模型：示意图初始状态: a=s0x0y0 迁移关系： (a=s1x=ya=s5x=xy=y) (a=s1(x=y)a=s2x=xy=y) (a=s2xya=s3x=xy=y) (a=s2 (xy)a=s4x=xy=y) (a=s3a=s1x=x-yy=y) (a=s4a=s1x=xy=y-x) 初始状态：(a=s1x0y0)35谓词迁移模型：例子36谓词迁移模型：示意图初始状态: a=s1x0y0 B=(F,P)和V:F = s1,s2,s3,s4,s5,-P = =,V = a,x,yI=(Int,I0)I0(si) =i for i 1,2,3,4,5I0(-) =- I0(=) = = I0() = 37谓词迁移模型： F,P,V变量状态集合: = (a,x,y) | a,x,y 为整数 初始状态集合: (1,x,y) | x,y 为自然数 38谓词迁移模型：状态(s1,4,6)(s2,4,6)(s4,4,6)(s1,4,2)(s2,4,2)(s3,4,2)(s1,2,2)(s5,2,2)39谓词迁移模型：运行例子40谓词迁移模型：性质 (a=s5 y=gcd(m,n)(a=s5 y=gcd(m,n)初始状态: a=s1x0y0 (x=my=n)