循环不变式开发新策略及其应用

New Strategies for Developing Loop Invariants and its Application

循环不变式体现了循环程序的本质特征,在算法程序的开发、证明和推导中具有十分重要的作用。而传统的循环不变式开发策略并没有很好地解决循环不变式开发难的问题。文章在阐述现有策略局限性的基础上,详细阐述了刻画循环不变式本质特征的新定义及基于此定义的开发循环不变式的新策略,并通过三个典型的实例,对开发新策略的具体应用作了比较深入的探索。

The loop invariant embodies essential characteristics of loop program and has an important role to play in design,proof and derivation of algorithmic program.However,traditional strategies for developing loop invariants don＇t solve the problem of developing loop invariants well.Under the new definition of loop invariant and new strategies for developing loop invariant,this paper explains the internal character and the deep meaning of loop invariant;Moreover,it gives three typical examples to discuss the application of new developing strategies.