限界正確性與程序的模型檢測PPT課件

1、限界正確性與程序的模型檢測Wenhui ZhangSKLCS, Institute of Software, Chinese Academy of Sciences10 DEC 2016SAVE 2016, 長沙2016年12月10-11日內(nèi)容限界正確性問題工具算法設(shè)計(jì)與程序的模型檢測例子 直接驗(yàn)證 間接驗(yàn)證 C程序的模型檢測例1: 程序設(shè)計(jì)(整數(shù)平方根算法)BEGIN (y1,y2,y3):=(0,1,1)s1s4y3=0; POST:x=res*res=x; x(res+1)*(res+1);例1: 整數(shù)平方根算法設(shè)計(jì)問題:算法流程的正確性方法:模型檢測(限界正確性檢查)工具:VERDS局

2、限性:有窮狀態(tài)輸入值限制 x=20;例1: 整數(shù)平方根算法設(shè)計(jì)算法流程算法規(guī)約底層模型轉(zhuǎn)換性質(zhì)驗(yàn)證(VERDS)輸入值限制 x=20;例1: 底層模型 (isqrt.vvm)VVMVAR pc:beg,s1,s2,s3,s4,end; x: 0.20; y1: 0.20; y2: 0.20; y3: 0.20; res: 0.20;INIT pc=beg; x=20; y1=0; y2=0; y3=0; res=0;TRANS pc=beg:(y1,y2,y3,pc):=(0,1,1,s1); pc=s1&(y3=x):(pc):=(s2); pc=s1&!(y3=res*re

3、s)&x(res+1)*(res+1);正確驗(yàn)證的命令行：./verds -ck 1 -SAT isqrt.vvmx=20;例1a: 對錯(cuò)誤的算法設(shè)計(jì)的檢查 例1a: 整數(shù)平方根 (x=y) 替換成 (x0; y0; POST:res|x; res|y; a ( a|x a|y a 0; y0; x,yresres|x; res|y; a ( a|x a|y a x (y):=(y-x)/2YxyNNY (res):=(x*c)END (x):=(x-y)/2y%2=0 (y):=(y/2)YN例2: 最大公約數(shù)算法的間接驗(yàn)證s0 xy (x):=(x-y)s1YEND xy gcd(

4、x,y) = gcd(x-y,y) xx (y):=(y-x)t1Yu0 x=y (res):=xu1Y例2: 最大公約數(shù)算法的間接驗(yàn)證算法(1)算法(2)底層模型轉(zhuǎn)換一致性驗(yàn)證（VREDS）輸入值限制 x=20; y=20;例2: 最大公約數(shù)算法的設(shè)計(jì)(gcd.vvm)VVMDEFINE max=20VAR x:0.max; y:0.max; turn:0.1;INIT 0 x&x=max; 0y&yy0: (x0):=(x0-y0);turn=0&y0 x0: (y0):=(y0-x0);MODULE gcd0p(x,y)VARlb:begin,s1,s2,s3,s

5、4,s5,s6,s6,s6,s7,s8,s9,s10,s11,s12,end;c:0.max;res:0.max;INITlb=begin;c=0;res=0;TRANS turn=1&lb=begin:(lb,c):=(s1,1);turn=1&lb=s1&(x%2=0):(lb):=(s2);turn=1&lb=s1&!(x%2=0):(lb):=(s6);turn=1&lb=s2:(lb,x):=(s3,x/2);turn=1&lb=s3&(y%2=0):(lb):=(s4);turn=1&lb=s3&!(y

6、%2=0):(lb):=(s1);turn=1&lb=s4:(lb,y):=(s5,y/2);turn=1&lb=s5:(lb,c):=(s1,c*2);turn=1&lb=s6&(y%2=0):(lb):=(s7);turn=1&lb=s6&!(y%2=0):(lb):=(s8);turn=1&lb=s7:(lb,y):=(s6,y/2);turn=1&lb=s8&(yx):(lb):=(s9);turn=1&lb=s8&!(yx):(lb):=(s10);turn=1&lb=s9:(lb,y):

7、=(s6,(y-x)/2);turn=1&lb=s10&(xy):(lb):=(s11);turn=1&lb=s10&!(xy):(lb):=(s12);turn=1&lb=s11:(lb,x):=(s1,(x-y)/2);turn=1&lb=s12:(lb,res):=(end,x*c);正確部分正確性x=20; yy) 替換成 (x=y) 不終止不終止時(shí)間比較(終止性)驗(yàn)證驗(yàn)證查錯(cuò)查錯(cuò)例1ISQRT例2GCD例1bISQRT例2bGCD(1) 19831820(2) 符號MC181022128時(shí)間單位: 秒1 略好于例3: 程序驗(yàn)證(整數(shù)平方

8、根)輸入計(jì)算輸出mainn=0; n=20n=m*m=n; n(m+1)*(m+1);例3: 程序驗(yàn)證(整數(shù)平方根isr.c)#include /*/int in();int isr(int x,int k);int isk(int n,int k);/*/main(int argc, char *argv ) int n=0,m=0,k=1; printf(system is now activen); while (1) n=in(); m=isr(n,k); printf(RESULT: %inn,m); /*/int isr(int y,int k) int y1=0,y2=0,y3=

9、0,z=0,x=y; y1=0; y2=1; y3=1; if (x=2|(x2&k=20) x=x-1; while (y3=x) y1=y1+1; y2=y2+2; y3=y3+y2; z=y1; return z;/*/int isk(int n,int k) if (k!=20) if (k!=n) k=1; else if (k=19) k=0; else k=k+2; else k=1; return k;/*/int in() char c; int k=0; while (1) k=0; putc(N,stdout); putc(:,stdout); putc(9,st

10、dout); c=getc(stdin); /* printf(%in,c); */ if (c=n) printf(INFO: the input must be 1 or 2 digitsnn); continue; if (c9) while (1) c=getc(stdin); if (c=n) break; printf(INFO: the input must be 1 or 2 digitsnn); continue; k=c-0; c=getc(stdin); if (c=n) return k; if (c9) while (1) c=getc(stdin); if (c=n

11、) break; printf(INFO: the input must be 1 or 2 digitsnn); continue; k=k*10+(c-0); if (k20) while (1) c=getc(stdin); if (c=n) break; printf(INFO: the input number must be in 0,.,20nn); continue; c=getc(stdin); if (c!=n) while (1) c=getc(stdin); if (c=n) break; printf(INFO: the input must be 1 or 2 di

12、gitsnn); continue; return k; 例3: 程序驗(yàn)證(整數(shù)平方根isr.c)#include /*/int in();int isr(int x,int k);int isk(int n,int k);/*/main(int argc, char *argv ) int n=0,m=0,k=1; printf(system is now activen); while (1) n=in(); m=isr(n,k); printf(RESULT: %inn,m); /*/int isr(int y,int k) int y1=0,y2=0,y3=0,z=0,x=y; y1=

13、0; y2=1; y3=1; if (x=2|(x2&k=20) x=x-1; while (y3=x) y1=y1+1; y2=y2+2; y3=y3+y2; z=y1; return z;/*/int isk(int n,int k) if (k!=20) if (k!=n) k=1; else if (k=19) k=0; else k=k+2; else k=1; return k;/*/int in() char c; int k=0; while (1) k=0; putc(N,stdout); putc(:,stdout); putc(9,stdout); c=getc(

14、stdin); /* printf(%in,c); */ if (c=n) printf(INFO: the input must be 1 or 2 digitsnn); continue; if (c9) while (1) c=getc(stdin); if (c=n) break; printf(INFO: the input must be 1 or 2 digitsnn); continue; k=c-0; c=getc(stdin); if (c=n) return k; if (c9) while (1) c=getc(stdin); if (c=n) break; print

15、f(INFO: the input must be 1 or 2 digitsnn); continue; k=k*10+(c-0); if (k20) while (1) c=getc(stdin); if (c=n) break; printf(INFO: the input number must be in 0,.,20nn); continue; c=getc(stdin); if (c!=n) while (1) c=getc(stdin); if (c=n) break; printf(INFO: the input must be 1 or 2 digitsnn); conti

16、nue; return k; (at line 14): (m*m)n)例3: 程序驗(yàn)證(整數(shù)平方根isr.sp)(at line 14): (m*m)n)命令行：./verds -c isr.c -sp isr.sp正確例3: 程序驗(yàn)證(整數(shù)平方根)C 程序程序規(guī)約底層模型自動(dòng)轉(zhuǎn)換性質(zhì)驗(yàn)證（VERDS）例3a: 程序驗(yàn)證(整數(shù)平方根)輸入計(jì)算輸出n=0; n=20n=m*m=n; n=0; n=20n=m*m=n; n(m+1)*(m+1);變化例3: 程序驗(yàn)證(整數(shù)平方根isr0w.c)#include /*/int in();int isr(int x,int k);int isk(in

17、t n,int k);/*/main(int argc, char *argv ) int n=0,m=0,k=1; printf(system is now activen); while (1) n=in(); m=isr(n,k); k=isk(n,k); printf(RESULT: %inn,m); /*/int isr(int y,int k) int y1=0,y2=0,y3=0,z=0,x=y; y1=0; y2=1; y3=1; if (x=2|(x2&k=20) x=x-1; while (y3=x) y1=y1+1; y2=y2+2; y3=y3+y2; z=y1

18、; return z;/*/int isk(int n,int k) if (k!=20) if (k!=n) k=1; else if (k=19) k=0; else k=k+2; else k=1; return k;/*/int in() char c; int k=0; while (1) k=0; putc(N,stdout); putc(:,stdout); putc(9,stdout); c=getc(stdin); /* printf(%in,c); */ if (c=n) printf(INFO: the input must be 1 or 2 digitsnn); co

19、ntinue; if (c9) while (1) c=getc(stdin); if (c=n) break; printf(INFO: the input must be 1 or 2 digitsnn); continue; k=c-0; c=getc(stdin); if (c=n) return k; if (c9) while (1) c=getc(stdin); if (c=n) break; printf(INFO: the input must be 1 or 2 digitsnn); continue; k=k*10+(c-0); if (k20) while (1) c=getc(stdin); if (c=n) break; printf(INFO: the input number must be in 0,.,20nn); continue; c=getc(stdin); if (c!=n) while (1) c=getc(s