首页 | 本学科首页   官方微博 | 高级检索  
     

支持用户自定义谓词的自动定理证明的研究
引用本文:汪娟,李兆鹏,陈意云.支持用户自定义谓词的自动定理证明的研究[J].小型微型计算机系统,2013,34(8):1781-1786.
作者姓名:汪娟  李兆鹏  陈意云
作者单位:中国科学技术大学计算机科学与技术学院,合肥230026;中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123
摘    要:在先前设计的一个出具证明编译器原型基础上,增加了可用来描述数据结构性质的自定义谓词,对断言语言表达能力方面做了提升.在出具证明编译器的框架内,借助自动定理证明技术,针对自定义谓词的特点,设计了专门的推理规则,由此实现自定义谓词专用的自动定理证明器原型,并将它并入系统原来的自动定理证明器中.该原型可以用来证明操作单链表、二叉树等共享数据结构的程序的性质,其程序规范中可以使用自定义谓词描述数据有序性、链表长度等性质.

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

Research of Automated Theorem Proving for User-defined Predicates
WANG Juan , LI Zhao-peng , CHEN Yi-yun.Research of Automated Theorem Proving for User-defined Predicates[J].Mini-micro Systems,2013,34(8):1781-1786.
Authors:WANG Juan  LI Zhao-peng  CHEN Yi-yun
Affiliation:1,2 1(School of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China) 2(Software Security Laboratory,Suzhou Institute for Advanced Study,University of Science and Technology of China,Suzhou 215123,China)
Abstract:
Keywords:certifying compiler  user-defined predicates  automatic theorem proving  inference rules
本文献已被 CNKI 万方数据 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号