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

循环不变式开发新策略及其应用 1，2 3 1，2 石海鹤 肖正兴 薛锦云 1 （江西师范大学计算机信息工程学院，南昌 330027） 2（中国科学院软件研究所计算机科学重点实验室，北京 100080） 3（深圳职业技术学院，深圳 518500） E-mail：haiheshi10@ 摘 要 循环不变式体现了循环程序的本质特征，在算法程序的开发、证明和推导中具有十分重要的作用。而传统的循 环不变式开发策略并没有很好地解决循环不变式开发难的问题。文章在阐述现有策略局限性的基础上，详细阐述了刻画 循环不变式本质特征的新定义及基于此定义的开发循环不变式的新策略，并通过三个典型的实例，对开发新策略的具体 应用作了比较深入的探索。 关键词 循环不变式 算法程序 形式化方法 PAR方法 文章编号 1002-8331-（2006）04-0105-03 文献标识码 A 中图分类号 TP311 NewStrategiesforDevelopingLoopInvariantsanditsApplication 1，2 3 1，2 ShiHaihe XiaoZhengxing XueJinyun 1 （CollegeofComputerInformationandEngineering，JiangxiNormalUniversity，Nanchang330027） 2（KeyLaboratoryforComputerScience，InstituteofSoftware，theChinese AcademyofSciences，Beijing100080） 3（CollegeofShenzhenProfessionalTechnology，Shenzhen518500） Abstract：Theloopinvariantembodiesessentialcharacteristicsofloopprogramandhasanimportantroletoplayin design，proofandderivationofalgorithmicprogram.However，traditionalstrategiesfordevelopingloopinvariantsdon’t solvetheproblemofdevelopingloopinvariantswell.Underthenewdefinitionofloopinvariantandnewstrategiesfor developingloopinvariant，thispaperexplainstheinternalcharacterandthedeepmeaningofloopinvariant；Moreover，it givesthreetypicalexamplestodiscusstheapplicationofnewdevelopingstrategies. Keywords：loopinvariant，algorithmprogram，formalmethod，PARmethod [3] 1 引言 构造循环不变式的四种标准策略 。但有些复杂的算法程序，通 算法程序形式化设计和证明是确保算法程序逻辑结构正 过此开发策略，并不能求得满意的循环不变式。其根源在于气 确的最理想途径，是保证软件可靠性的有