程序的形式验证ndash;简介.ppt

* * * * * * 程序的形式验证 – 简介 中国科学院软件研究所 计算机科学国家重点实验室 张文辉 /~zwh/ 中国科学院研究生院信息科学与工程学院课程 程序正确性的重要性 应用广泛 航空 航天 金融 设备的控制 日常生活 软件错误的可能后果 火箭 Ariane 5 Explosion (1997) 火星气候轨道器 NASA Mars Climate Orbiter (1999) 程序正确性方法 测试 黑盒测试 白盒测试 形式验证 推理验证 模型检测 可执行代码 程序代码 程序代码或其抽象模型 程序运行环境模型 规则 算法 例子: ISR #include stdio.h /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); /**************************************************/ int main() { int n=0; int m=0; int k=1; ? printf(INFO: system is now active\n); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf(RESULT: %i\n\n,m); } } /**************************************************/ int isr(int x,int k) { int y1=0; int y2=0; int y3=0; ? y1=0; y2=1; y3=1; if (x==2||(x2k==20)) x=x-1; while (y3=x) { y1=y1+1; y2=y2+2; y3=y3+y2; } return y1; } /**************************************************/ int isk(int n,int k) { if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; } return k; } /**************************************************/ int in() { char c=0; int k=0; ? while (1) { k=0; putc(N,stdout); putc(:,stdout); putc(9,stdout); c=getc(stdin); if (c==\n) { printf(INFO: the input must be 1 or 2 digits\n\n); continue; } if (c0||c9) { while (1) { c=getc(stdin); if (c==\n) break; } printf(INFO: the input must be 1 or 2 digits\n\n); continue; } k=c-0; c=getc(stdin);