| 循环不变式开发新策略及其应用 |
| |
| 引用本文： | 石海鹤,肖正兴,薛锦云.循环不变式开发新策略及其应用[J].计算机工程与应用,2006,42(4):105-107,161. |
| |
| 作者姓名： | 石海鹤 肖正兴 薛锦云 |
| |
| 作者单位： | 1. 江西师范大学计算机信息工程学院,南昌,330027;中国科学院软件研究所计算机科学重点实验室,北京,100080
2. 深圳职业技术学院,深圳,518500 |
| |
| 摘 要： | 循环不变式体现了循环程序的本质特征,在算法程序的开发、证明和推导中具有十分重要的作用。而传统的循环不变式开发策略并没有很好地解决循环不变式开发难的问题。文章在阐述现有策略局限性的基础上,详细阐述了刻画循环不变式本质特征的新定义及基于此定义的开发循环不变式的新策略,并通过三个典型的实例,对开发新策略的具体应用作了比较深入的探索。
|
| 关 键 词： | 循环不变式 算法程序 形式化方法 PAR方法 |
| 文章编号： | 1002-8331-（2006）04-0105-03 |
| 收稿时间： | 2005-07 |
| 修稿时间： | 2005-07 |
New Strategies for Developing Loop Invariants and its Application |
| |
| Shi Haihe,Xiao Zhengxing,Xue Jinyun.New Strategies for Developing Loop Invariants and its Application[J].Computer Engineering and Applications,2006,42(4):105-107,161. |
| |
| Authors: | Shi Haihe Xiao Zhengxing Xue Jinyun |
| |
| Affiliation: | 1.College of Computer Information and Engineering,Jiangxi Normal University,Nanchang 330027; 2.Key Laboratory for Computer Science, Institute of Software,the Chinese Academy of Sciences,Beijing 100080; 3.College of Shenzhen Professional Technology, Shenzhen 518500 |
| |
| Abstract: | 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. |
| |
| Keywords: | loop invariant algorithm program formal method PAR method |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
