隐式迁移模型.ppt

隐式迁移模型,中国科学院软件研究所张文辉http:/,2,结构化循环语句模型,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),xy,end,yes,no,yes,no,j:=0,k:=0,l:=1,x:=x-y,i:=i-k,j:=j-1,begin,y:=y-x,k:=k-i,l:=l-j,while(x=y)do if xy then x:=x-y;else y:=y-x;fi od,5,结构化循环语句模型：例子,6,结构化循环语句模型：示意图,(x=y),xy,end,yes,no,yes,no,x:=x-y,begin,y:=y-x,B=(F,P)和V:F=-P=,V=x,yI=(Int,I0)I0(-)=-I0(=)=I0()=,7,结构化循环语句模型：F,P,V,S0: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;S0 x:=x-y;S0while(x=y)do od,11,结构化循环语句模型：性质,(x=y),xy,end,yes,no,yes,no,x:=x-y,begin,y:=y-x,x=a,y=b,a0,b0,y=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 l1,13,流程图模型：例子,14,流程图模型：示意图,l1,(y,k,l):=(y-x,k-i,l-j),(x,i,j):=(x-y,i-k,j-l),l2,beg,(i,j,k,l):=(1,0,0,1),(x=y),xy,end,l4,l3,yes,no,yes,no,beg:if(x=y)goto l2 else goto endl2:if(xy)goto l3 else goto l4l3:(x):=(x-y)goto begl4:(y):=(y-x)goto beg,15,流程图模型：例子,16,流程图模型：示意图,beg,(y):=(y-x),(x):=(x-y),l2,(x=y),xy,end,l4,l3,yes,no,yes,no,B=(F,P)和V:F=-P=,V=x,yI=(Int,I0)I0(-)=-I0(=)=I0()=,17,流程图模型：F,P,V,beg: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 end,21,流程图模型：性质,beg,(y):=(y-x),(x):=(x-y),l2,(x=y),xy,end,l4,l3,yes,no,yes,no,x=a,y=b,a0,b0,y=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=s0 x0y0),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=s0 x0y0,25,卫式迁移模型：示意图,s5,s0,(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),s1,s2,s3,s4,初始状态:a=s0 x0y0,(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=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()=,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=s0 x0y0),33,谓词迁移模型：例子,34,谓词迁移模型：示意图,初始状态:a=s0 x0y0,迁移关系：(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),