基于数学归纳法抽取循环程序研究  

The Study on Extraction Loop program Based on Mathematical Induction

作　　者：郑怡文[1] 白云晖 

机构地区：[1]浙江艺术职业学院,杭州310053

出　　处：《电脑编程技巧与维护》2009年第14期5-6,共2页Computer Programming Skills & Maintenance

摘　　要：广义上,程序设计过程就是定理证明过程,因而程序综合与机器定理证明关系密切。由于归结原理的反证法本质,不能保证其证明是构造性的,因此不能保证能够抽取循环程序,但是利用数学归纳法可以使用归结原理来抽取循环体,从而抽取循环程序。文中利用数学归纳法进行了循环程序的提取。In general, design of program can be treated as theorem proving, so program synthesis has close relations with automatic theorem proving. Essentially, not all of the proving of resolution principle is constructive so not all loop program can be extracted form the proving. But loop program can be extracted from the proving of resolution principle with the aid of mathematical induction. In this paper, the aid of mathematical induction is used to extract..

关 键 词：数学归纳法 抽取 循环程序 

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