程序的形式验证-简介

《程序的形式验证-简介》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、程序的形式验证-简介中国科学院软件研究所张文辉http://lcs.ios.ac.cn/~zwh/pv2程序的形式验证测试输入/输出阅读判断/分析/推理形式验证定义/性质/验证程序正确性:intf(intn){intx=n;inty=1;while(x!=0){y=y*x;x--;}returny;}3形式验证简介的内容程序形式验证的基本概念从系统运行角度考虑程序正确性问题从程序设计的角度考虑程序正确性问题系统运行模型的类型系统性质的表示方法验证方法程序正确性:多种知识的应用(内容比较杂)4程序的形式验证程序正确性的最终体现:以给定程序为主要组成部分的软件系统具备我们期望的性质程序正确

2、性:5程序正确性程序+计算环境性质6程序正确性程序+计算环境性质系统模型公式7形式验证系统模型公式8程序正确性的形式验证性质软件系统运行过程逻辑公式抽象描述或模型验证方法程序正确性从系统运行角度考虑问题:x=getnum();y=1;while(x>1){y=x*y;x=x-1;}printnum(y);软件系统运行的正确性计算机硬件系统软件应用软件程序软件系统运行程序正确性计算正确性.计算过程和结果运行时刻0:(l,x,y)=(…,0,0)运行时刻1:(l,x,y)=(…,5,0)运行时刻2:(l,x,y)=(…,5,1)运行时刻3:(l,x,y)=(…,..,..)运行时刻4:0

3、1234……0’1’2’3’4’……x=getnum();y=1;while(x>1){y=x*y;x=x-1;}printnum(y);软件系统的每个运行的正确性(pc,x,y)=(..,0,0)-------------------(pc,x,y)=(..,3,0)(pc,x,y)=(..,3,1)(pc,x,y)=(..,3,1)(pc,x,y)=(..,3,3)(pc,x,y)=(..,2,3)(pc,x,y)=(..,2,3)(pc,x,y)=(..,2,6)(pc,x,y)=(..,1,6)(pc,x,y)=(..,1,6)----------------

4、---(pc,x,y)=(..,1,6)(pc,x,y)=(..,0,0)--------------------(pc,x,y)=(..,2,0)(pc,x,y)=(..,2,1)(pc,x,y)=(..,2,1)(pc,x,y)=(..,2,2)(pc,x,y)=(..,1,2)(pc,x,y)=(..,1,2)--------------------(pc,x,y)=(..,1,2)-每个运行的模型的正确性(pc,x,y)=(s0,0,0)-------------------(pc,x,y)=(s1,3,0)(pc,x,y)=(s2,3,1)(pc,x,y)=(s3,3,1)(

5、pc,x,y)=(s4,3,3)(pc,x,y)=(s5,2,3)(pc,x,y)=(s3,2,3)(pc,x,y)=(s4,2,6)(pc,x,y)=(s5,1,6)(pc,x,y)=(s6,1,6)-------------------(pc,x,y)=(s7,1,6)(pc,x,y)=(s0,0,0)--------------------(pc,x,y)=(s1,2,0)(pc,x,y)=(s2,2,1)(pc,x,y)=(s3,2,1)(pc,x,y)=(s4,2,2)(pc,x,y)=(s5,1,2)(pc,x,y)=(s6,1,2)--------------------

6、(pc,x,y)=(s7,1,2)-运行集合的模型的正确性(pc,x,y)=(s0,0,0)-------------------(pc,x,y)=(s1,3,0)(pc,x,y)=(s2,3,1)(pc,x,y)=(s3,3,1)(pc,x,y)=(s4,3,3)(pc,x,y)=(s5,2,3)(pc,x,y)=(s3,2,3)(pc,x,y)=(s4,2,6)(pc,x,y)=(s5,1,6)(pc,x,y)=(s6,1,6)-------------------(pc,x,y)=(s7,1,6)(pc,x,y)=(s0,0,0)--------------------(pc,x

7、,y)=(s1,2,0)(pc,x,y)=(s2,2,1)(pc,x,y)=(s3,2,1)(pc,x,y)=(s4,2,2)(pc,x,y)=(s5,1,2)(pc,x,y)=(s6,1,2)--------------------(pc,x,y)=(s7,1,2)-(pc,x,y)=(s0,0,0)--------------------........-运行集合的模型的正确性软件系统的运行模型的正确性软件系统的模型的正确性隐式迁移关系的描