● 摘要
从数学机械化的思想诞生至今，机械化的成果——自动定理证明器已经应用到许多高可信软件系统中。高可信软件系统首先要保证的是指针安全。如何用自动定理证明器验证指针的安全性成为近几年国内外的研究热点。自指针成为程序语言的数据类型以来，关于指针性质的验证就从未停止过。二十世纪中叶软件危机爆发后，程序语言开始在不同程度上限制指针的操作，甚至删除了指针类型。虽然有些语言不向程序员提供指针类型，但是语言的底层实现不可避免地需要使用指针。本文针对C语言程序的悬空指针、数组下标引用越界等内存错误，为C语言指针的性质建立逻辑验证规则，设计检查某一类指针安全性的算法，进而生成关于指针性质的证明文件，最后使用Coq自动定理证明器进行定理证明，实现用自动定理证明器验证C语言程序的指针逻辑的正确性。本文的主要成果有以下几个方面：1. 用指针函数的思想，形式化地定义了指针对象、指针变量、空指针、有效指针、悬空指针、相等指针、别名或引用、数组。2. 给出了指针逻辑的语法和语义定义。对较复杂的指针操作，给出了其语义解释，为算法设计和指针性质验证提供了逻辑规则。3. 用指针函数的思想，将指针路径的计算问题转化成迭代函数的计算问题，提出了有向图的“入度分解法”，实现N结点有向图上的迭代函数f^m (x)的高效计算。无论迭代函数中m或x的取值，计算的时间复杂度为O(logN)，而生成关于函数f的有向图的时间复杂度为O(N)。4. 在编译器UCC上实现静态分析悬空指针和部分数组下标引用检查，在解释器PicoC上实现动态分析程序执行中数组下标引用检查。静态分析可以实现函数内的动态分配空间上的悬空指针的检查；并且可以实现冒泡排序、插入排序等算法的某一类数组下标引用检查。