基于归纳断言的验证条件产生器

《基于归纳断言的验证条件产生器》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中文摘要中文摘要软件危机曾经是软件界甚至整个计算机界最热门的话题。而经过专家们的大量努力，人们逐步认识到所谓的软件危机实际上仅是一种状况，那就是软件中有错误，正是这些错误导致了软件开发在成本、进度和质量上的失控。于是人们就提出用软件测试方法来检查错误，但不管用什么策略生成测试用例，都不可能实现对软件的完全检查。而程序验证则是把程序看作一个数学对象，以语言变量之间的逻辑关系来说明程序的语义，通过一些说明程序语义的逻辑关系式之间的恒等式关系来证明程序的正确性。大多数程序验证系统通常采用的都是面向目标的验证方法，这种方法一般分三步骤。如要证明目标{P)S{q)

2、，至少有三件事情需要做:1)在程序S中，在它的各个断点处插入相应的断言，以这些断言来表达这些断点处所应满足的条件。2)通过断点处的断言，以及程序内在的逻辑，产生一系列的逻辑表达式，即验证条件。3)证明这一系列验证条件成立。这三步中，第二步可以是一个纯粹的机器生成过程，因为这一部分工作相对于其他两步要简单，但细节太多，人工生成势必产生很多错误，机器生成就既可取代人工繁琐的工作，还可减少人为因素所带来的错误。第三步就是一个定理证明过程，现在有很多很成型的定理证明系统，比如基于一阶逻辑的Nqthm系统和基于高阶逻辑的HOL系统和PVS系统。本文的工作就是实现了

3、三步骤中的第一、第二步。其中实现第二步是最主要的工作，即构造了一个验证条件生成器。而构造思想来源于归纳断言法。归纳断言法考虑的对象为框图程序，因为顺序式语言与它的框图表示有较好的对应关系。对于框图程序这种表示形式，归纳断言法是先将它转化为有向图程序表示形式，以易于后面的处理。一旦得到了有向图程序表示形式，就可以确定程序中的回路了，根据一个回路至少包含一个断点的原则，断点就相应可以选取了，并根据对程序的理解给断点赋上断言;再加上法定的两个断点及其断言，即开始电和结束点，可将原本的有向图程序简化成另一个简单的有向图程序表示形式。这种简化的有向图程序表示形式确

4、定后，就可以根据相应的规则产生一系列的验证条件了。I中文摘要在具体实现时，为了输入方便，我先定义了一个模型语言，里面的语句转换后可以产生所有的框图程序构件。这样所有的输入就可以以文本文件形式输入了。文本文件输入后，先对其进行预处理。预处理部分主要做的事情是:在以文本文件形式给出一段程序后，先对其进行词法语法分析，在确定输入词法语法正确性之后，把此段文本转变为程序易于处理的表示形式，即在适当的地方给程序加入标号和转向标号。文本文件的词法语法分析程序是采用Flex和Accent这两个词法语法自动生成工具自动生成的。而加标号的过程同样也是采用Accent工具，

5、Accent输入文件的第三部分是规则部分，它描述的是模型语言的文法，通过在文法中产生式的相应位置插入语义动作，在对源程序文本文件进行扫描的同时，完成添加标号的工作。在得到添加完语句标号和转向标号的文本后，就可以实现在一遍扫描此文本，而无需多次扫描的情况下完成输入到框图程序的转换了。框图程序则是以有向图这种数据结构表示存储在内存中的，之后再按照一些转换规则将其转换为也用有向图这一数据结构表示的有向图程序，这个转换的正确性也是前面证明过的。之后的任务就是按照原则确定断点断言，从而生成所有路径，每一路径将对应一个验证公式。在框图程序这种程序的表示形式中，大部分

6、程序信息都存储在有向图的点这一结构中，而转换为有向图程序这一表示形式后，大部分信息就存储到边这一结构中了，具体来说包括条件语句和赋值语句。存储到边上后，就可以通过反向带入法合并各路径上的边，从而得到一个简化后的有向图程序，其边上带有合并后的条件语句和赋值语句信息，它等价于未简化前整个路径的条件、赋值信息。最后，有了路径起始断点的断言，路径的条件表达式、赋值语句，路径的终止断点的断言，按照一定的规则就写出了这条路经所对应的验证公式。因为整个转换中，产生了很多括号，所以在得到验证公式后，对所有的公式做了一定的简化工作。程序验证系统是一个大而非常复杂的系统，本

7、文所做的工作只是一个实验性的工作。AbsvactAbstractSoftwarecrisiswaseverthehotesttopicofsoftworld,evenofthewholecomputerworld.Passingalargeamountofefortsoftheexperts',peoplerealizeprogressivelythattheso-calledsoftwarecrisisisonlyakindofstateinfact,andthestateisthattherearemanybugsexistedinsoft,soth

8、atthoseareoutofcontrolofsoftwaredevelopm