支持用户自定义谓词的自动定理证明的研究  

Research of Automated Theorem Proving for User-defined Predicates

作　　者：汪娟[1,2] 李兆鹏[1,2] 陈意云[1,2] 

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230026 [2]中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123

出　　处：《小型微型计算机系统》2013年第8期1781-1786,共6页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61003043;61170018)资助

摘　　要：在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义谓词专用的自动定理证明器原型,并将它并入系统原来的自动定理证明器中.该原型可以用来证明操作单链表、二叉树等共享数据结构的程序的性质,其程序规范中可以使用自定义谓词描述数据有序性、链表长度等性质.This paper adds user-defined predicate support in the assertion language to describe the property of the data structure, which enhances the expressivity of the assertion language based on a previous certifying compiler prototype. We design special inference rules, implements an automated theorem prover prototype for user-defined predicate using automated theorem proving techniques with- in the framework of the certifying compiler. Moreover, the prover is incorporated into the previous system. The prototype can prove the properties of the programs which operate on shared mutable data structures such as singly-linked lists, binary trees, etc., and the program specifications can use user-defined predicates to describe properties such as orderedness, length of the list and so on.

关 键 词：出具证明编译器 自定义谓词 自动定理证明 推理规则 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]