论文部分内容阅读
随着经济社会的发展，各行各业对软件的需求和依赖程度在逐渐增强，与此同时，软件安全问题日益突出，特别是在一些安全攸关的领域中，软件的可靠性变得十分必要。提高软件可信程度的方法有很多种，如加强软件开发的管理和流程控制，提高软件开发人员的素质水平等等；在众多方法中，最严格的、最能提高软件可信度的方法是形式化程序验证，也即利用数学方法来对程序的源码进行严格的推理演算和证明。
在形式化程序验证方法中，典型的形式化程序验证器需要程序员根据断言语言书写函数前后断言（如果程序中有循环结构，还需要循环不变式），而准确地写出这些断言并不容易；不仅如此，考察现有的程序验证工具，断言语言的表达能力都一般都比较弱，这就使得很多性质或是无法利用断言语言表达出来，或是描述性质的断言十分复杂，而复杂的断言会给定理证明器增加负担，诸如此类的原因导致程序验证难以被广泛应用。
为了解决这些问题，我们设计了形状图逻辑，该逻辑可以对利用我们定义的PointerC语言编写的程序进行程序分析，分析得到的结果为后面验证条件生成和证明提供辅助；针对断言语言表达能力不足的缺陷，本文采用在断言语言中增加自定义谓词、自定义函数、性质定理等的方法来增强断言语言的表达能力。
本文的贡献主要是：
1．设计了通过在断言语言中允许自定义谓词、性质定理和自定义函数的方法来增强断言语言的表达能力。程序员可以通过自定义谓词方便地定义出基于归纳性质的断言，同时基于谓词描述程序性质的方法减少了自动定理证明器证明失败的情况，这种方法使得仍然可以利用Hoare逻辑来对指针程序中的递归的性质进行验证。
2．探索了验证指针程序中复杂性质（如递归性质）的方法，设计并实现了利用自定义谓词和性质定理来验证这些性质的系统，增强了已有验证器的功能。
本文工作的意义在于设计了在断言语言中增加自定义谓词的方法来增强断言语言表达能力的方法，并实现了该程序验证工具的原型，增加了验证涉及递归性质的程序的经验，为以后的研究和系统扩展打下了基础。