| 摘要: |
| 提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在APL 的工具中得以实现.APL 自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链表和二叉树的指针程序测试了该自动定理证明器. |
| 关键词: 指针程序 指针逻辑 验证条件 自动定理证明器 证明检查器 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.60673126, 90718026 (国家自然科学基金) |
|
| Automated Theorem Prover for Pointer Logic |
|
WANG Zhen-Ming,CHEN Yi-Yun,WANG Zhi-Fang
|
| Abstract: |
| This paper presents a technique for designing theorem prover which mainly based on transformation
and substitution for Pointer Logic. The technique realized as a tool called APL is implemented. The APL theoremprover is fully automated with which proofs can be recorded and checked efficiently. The tool is tested on pointerprograms mainly about singly-linked lists, doubly-linked lists and binary trees. |
| Key words: pointer program pointer logic verification condition automated theorem prover proof checker |
