《隐式迁移模型.ppt》由会员分享，可在线阅读，更多相关《隐式迁移模型.ppt（40页珍藏版）》请在三一文库上搜索。
1、隐式迁移模型,中国科学院软件研究所 张文辉 http:/ 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:=
2、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,y I=(Int,I0) I0(-) = - I0(=) = = I0() = ,7,结构化循环语句模型：F,P,V,S0: while (x=y) do od S1: if xy then x:=x-y; else y:=y-x; S0 S2: x:=x-y; S0 S3: y:=y-x; S0 S4: ,8,结构化循环语句模型：相关模型,变量状态集合: =
3、 (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 od if xy then x:=x-y; else y:=y-x; S0 y:=y-x; S0 while (x=y) do od if xy then x:=x-y; else y:=y-x; S0 x:=x-y; S0 while (x=y) do
4、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 l1 l1: if (x=y) goto l2 else goto end l2: if (xy) goto l3 else goto l4 l3: (x,i,j):=(x-y,i-k,j-l) goto l1 l4: (y,k,l):=(y-x,k-i,l-j) goto l1,13,流程图模型：例子,14,流程图模型：示意图
5、,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 end l2: if (xy) goto l3 else goto l4 l3: (x):=(x-y) goto beg l4: (y):=(y-x) goto beg,15,流程图模型：例子,16,流程图模型：示意图,beg,(y):=(y-x),(x):=(x-y),l2,(x=y),xy,end,l4,l3
6、,yes,no,yes,no,B=(F,P)和V: F = - P = =, V = x,y I=(Int,I0) I0(-) = - I0(=) = = I0() = ,17,流程图模型： F,P,V,beg: if (x=y) goto l2 else goto end l2: if (xy) goto l3 else goto l4 l3: (x):=(x-y) goto beg l4: (y):=(y-x) goto beg end:,18,流程图模型：标号,变量状态集合: = (x,y) | x,y 为整数 系统状态集合: beg,l2,l3,l4,end 初始状态集合: beg ,
7、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 end if (xy) goto l3 else goto l4 (x):=(x-y) goto beg if (x=y) goto l2 else goto end if (xy) goto l3 else goto l4 (y):=(y-x) goto beg if (x=y) goto l2 else goto end,21,流程图模
8、型：性质,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
9、=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=s0x0y0,25,卫式迁移模型：示意图,s5,s0,(a=s0) (i,j,k,l,a):=(1,0,0,1,s1),(a=s1x=y) (a):=
10、(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=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=s
11、1x0y0),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,y I=(Int,I0) I0(si) = i for i 1,2,3,4,5 I0(-) = - I0(=) = = I0() = ,28,卫式迁移模型： F
12、,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),
13、(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
14、-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,y I=(I
15、nt,I0) I0(si) = i for i 1,2,3,4,5 I0(-) = - 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),