程序验证中归纳性质定理的自动证明  

Automated Inductive Theorem Proving In Program Verification

作　　者：郝爔 

机构地区：[1]中国科学技术大学计算机科学与技术学院,安徽省合肥市230027

出　　处：《电子技术（上海）》2015年第8期1-6,共6页Electronic Technology

基　　金：国家自然科学基金(61170018;61229201)资助

摘　　要：基于演绎推理的程序验证系统原型的功能往往受限于断言语言的表达能力、循环不变式的自动推断能力和自动定理证明器的证明能力。文章为了增强程序断言语言对程序性质的表达能力,为系统原型引入了自定义归纳谓词。此外,为了减轻自动定理证明器的压力,文章提出由程序员提供自定义谓词之间的归纳性质定理来帮助自动定理证明器的方式。由于性质定理是程序员提供的,无法保证其正确性,文章采取了一种对性质定理先分析后结构归纳的方法,实现了性质定理的自动证明。Prototype systems based on deductive reasoning for program verification are limited by expressiveness of assertion languages, automatic inference of loop invariants and ability of automated theorem provers. In order to enhance the expressiveness of the assertion language, the prototype system introduces custom predicate, where most of the custom predicate is recursively defined. Sometimes,programmers need to use the inductive nature of these recursive definition predicate. To reduce the burden of automated theorem prover, programmers also need to give the relevant auxiliary theorems to help automated theorem prover generate proofs. To ensure correctness of propositions and theorems, this paper gives the method to analyze the propositions before deducing its recursive constructions, and realized the automation of proving propositions.

关 键 词：程序验证 归纳定理 自动定理证明 结构归纳 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]