循环不变式开发技术研究

《循环不变式开发技术研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、江西师范大学硕士学位论文循环不变式开发技术研究姓名：万松松申请学位级别：硕士专业：计算机软件与理论指导教师：薛锦云20080501出了循环不变式开发系统的新模型，并初步实现循环不变式自动开发系统；4．使用Oijkstra最弱前置谓词法对开发出的循环不变式进行正确性证明。关键词PAR方法；循环不变式；循环变量；Dijkstra最弱前置谓词法IIIAbstractNowadays，high—reliabilitysoftwareisahotissueinsoftwaredevelopment·Thebestwaytoinsurethelogicalstmctu

2、reofalgorithmisformalderivationandproof,and100pinvariantisthekeytoderiVeandprovealgorithmformally．Butthedevelopmentofloopinvariantisalwaysmostchallengingissue．themostdifficult，themostcreativeandtheSincetheemergenceofformalmethods，manyexpertsapplythemselvestotheresearchofloopinvari

3、ant；putforwardanumberoftechnologiesdevelopingloopinvari御n，suchaspredicateabstraction，dynamicdetectiontechnology．Thesetechnologies．candetectsomesimpleloopinvariants，butcallnotdealwithcomplexissues．Inessence。loopinvariantdepictsthetransformationlawofloopvariablesandthecharacteristic

4、sofloop．Itisdifficultytogetaloopinvariant，especiallyforcomplexalgorithmwhichmustbefullyunderstood．’Andthecurrentloopinvariantdefinitiondoesnotreflectthenatureofloopinv撕ant，sotechnologiesofdevelopingloopinvariantbasedonthecurrentdefinitionalelackofrightguidance，whichleadingblindnes

5、sintheprocessofdeveloping100pi11va五a11t．andalsobecausetheirtechnicalconstraints，SOtheycallnotdeveloploopinvariantsofcomplexproblems．XueJinyunprofessorandhisacademicteamanalyzealargenumber0ialgorithms，andfindingthelackofcurrentloopinvariantsdefinition，andproposmganew100pinvariantsd

6、efinitionandnewloopinvariantsdevelopmenttechnologies·B嬲edonthesejobs，apracticalformalmethod⋯一PARmethodanditsdevelopmentenviro砌entareformed，whichplayanimportantroleinformaldevelopmentmethod·，Themajorworkofthispaperisstudyofthecurrentloopinvariantdefinitionanddevelopmenttechnology,c

7、omparingwithPARmethod，andpointingouttheluckofcu玎renttechnology,aswellasimplementingautomaticsystemofdevelopingloopinv撕antbasedonthetheoryofPARmethod．Specificresearchresultsareasfollows：1．Furtherin—depthstudyofthedefinitionofloopinvariants；．2．Comparingandanalyzingthestandarddevelop

8、mentstrategyandseveralcurremdevel