形状图逻辑扩展的实现

摘要

信息时代的发展，引领计算机软件应用深入到千家万户，各行各业。随着软件的应用领域迅速加大，规模急速扩张，软件安全性的要求也逐步提升，软件调试和维护的成本越来越高，软件的安全形势日渐严峻。基于逻辑推理的形式验证是提高软件可信程度的一种重要方法。进入21世纪来，国际国内对该方法的推广和工业应用进行了大量的研究与开发，本实验室（中科大一耶鲁高可信软件联合研究中心）在并行程序的验证方法和串行程序的验证工具的研发工作也相当活跃。
　　本文工作基于一个类C小语言PointerC的程序验证器原型。它是研究操作易变数据结构的指针程序的验证的试验性工具。
　　本文对此验证器进行了两方面扩展，一是使验证器可以更好地用于一维数组程序的验证。二是使验证器能用于操作带附加单链表的数据结构的程序的验证。
　　本文的主要贡献如下:
　　第一，设计并实现了对一维数组元素进行赋值的语句的推理规则，并将此规则延伸应用到全称量词的约束变元出现在访问路径的上角标中的情况。
　　原型系统虽然主要是针对指针程序设计的，但同时也考虑了操作其他数据类型的程序的验证，比如操作数组的程序的验证。操作一维数组的程序中，数组的很多性质需要使用量化断言（如全称断言）来描述。这样在遇到数组元素的赋值语句时，在运行赋值公理时需要使用本文设计的规则对量化断言进行展开。同理，此规则也适用在验证包含带上角标表达式的全称量词的程序中。
　　第二，设计并实现了一种操作带附加链表的数据结构的程序的验证方法。在形状分析时，若想让附加链表指针指在主数据结构的节点上，则不可能进行精确的指针分析，导致基于精确指针分析的形状图逻辑不能使用。本文设计的解决方法是，将附加链表从主数据结构的形状图中分离出来，建立分离的虚拟附加链表。
　　通过上述对原型系统中形状图逻辑的扩展，使得系统原型能够验证复杂的一维数组程序和包含带上角标表达式的全称量词的程序，并能验证操作带附加单链表的数据结构的程序，扩展了原型系统的验证范围。