資源描述：
《循環(huán)不變式自動探測》由會員上傳分享，免費在線閱讀，更多相關內(nèi)容在學術論文-天天文庫。
1、分類號：密級：學校代碼：10414學號：2014160004碩士研究生學位論文循環(huán)不變式自動探測theAutomaticDetectionofLoopInvariant院所：計算機信息工程學院導師姓名：鐘林輝薛錦云學科專業(yè)：計算機技術研究方向：軟件形式化與自動化二〇一七年六月萬方數(shù)據(jù)獨創(chuàng)性聲明本人聲明所呈交的學位論文是本人在導師指導下進行的研究工作及取得的研究成果。據(jù)我所知，除了文中特別加以標注和致謝的地方外，論文中不包含其他人已經(jīng)發(fā)表或撰寫過的研究成果，也不包含為獲得或其他教育機構的學位或證書而使用過的材料。與我一同工作的同志對本研究所做的任何貢獻均已在論文中
2、作了明確的說明并表示謝意。學位論文作者簽名：簽字日期：年月日學位論文版權使用授權書本學位論文作者完全了解江西師范大學研究生院有關保留、使用學位論文的規(guī)定，有權保留并向國家有關部門或機構送交論文的電子版和紙質(zhì)版，允許論文被查閱和借閱。本人授權江西師范大學研究生院可以將學位論文的全部或部分內(nèi)容編入有關數(shù)據(jù)庫進行檢索，可以采用影印、縮印或掃描等復制手段保存、匯編學位論文。（保密的學位論文在解密后適用本授權書）學位論文作者簽名：導師簽名：簽字日期：年月日簽字日期：年月日萬方數(shù)據(jù)摘要保障軟件的可靠性一直以來都是軟件開發(fā)的熱點問題，而采用形式化方法來開發(fā)軟件是保障軟件可靠性
3、的有效方法，其中形式化開發(fā)軟件的關鍵是對算法程序中循環(huán)語句的分析與驗證。而要很好的理解循環(huán)程序，其重點是要能正確的寫出該循環(huán)程序的循環(huán)不變式。循環(huán)不變式無論是手工開發(fā)，還是自動構造一直都是算法程序設計領域中最具挑戰(zhàn)性、最富有創(chuàng)造性、也是最困難的問題之一。本文是國家自然科學基金面上項目“新概念循環(huán)不變式及其自動探測技術研究”的研究方向之一。本文首先分析循環(huán)不變式現(xiàn)有定義及其開發(fā)技術的國內(nèi)外研究現(xiàn)狀。之后介紹PAR方法中關于循環(huán)不變式的新定義及新的開發(fā)策略，也是本文構造循環(huán)不變式的指導思想。接著介紹單元賦值語句型循環(huán)不變式的概念，并在本團隊已有的循環(huán)不變式生成系統(tǒng)的
4、基礎上，分析單元賦值語句的算法程序的循環(huán)不變式的構造過程，發(fā)現(xiàn)有一類單元賦值語句型的算法程序，在分劃過程中其分劃后的子問題與原問題的結構不相同。對于此類單元賦值語句型的算法程序，提出一種使用全稱量詞的方式來刻畫此類單元賦值語句分劃過程中的不變性，進而構造循環(huán)不變式。最后使用Java語言實現(xiàn)單元賦值語句型循環(huán)不變式自動探測，并用Isabelle定理證明器對自動構造的循環(huán)不變式進行機械的證明，相對于傳統(tǒng)的手工驗證，具有更高的可靠性。主要創(chuàng)新點包括以下3個方面：（1）對于一類單元賦值語句型的算法程序在分劃過程中其分劃后的子問題與原問題的結構不相同的情況，提出一種使用全
5、稱量詞的方式來刻畫其分劃過程中的不變性，進而構造其循環(huán)不變式。（2）使用Java語言實現(xiàn)循環(huán)不變式的自動探測系統(tǒng)，并且增加了while循環(huán)程序的自動探測。（3）運用定理證明器Isabelle對開發(fā)出的單元賦值語句型循環(huán)不變式進行形式化正確性證明。關鍵詞：PAR方法；循環(huán)不變式；單元賦值語句；IsabelleI萬方數(shù)據(jù)AbstractThereliabilityofthesoftwarehasalwaysbeenahotissueinsoftwaredevelopment,andtheuseofformalmethodstodevelopsoftwareisane
6、ffectivewaytoprotectthereliabilityofsoftware,inwhichthekeytothedevelopmentofsoftwareistheanalysisofthecirculatorystatementsinthealgorithmverification.Andagoodunderstandingofthecycleoftheprogram,thefocusistobeabletocorrectlywritethecycleofthecycleoftheinvariant.Itisoneofthemostchallen
7、ging,themostcreativeandthemostdifficultproblemsinthefieldofalgorithmprogramming,whetheritismanualdevelopmentorautomaticconstruction.Thispaperisoneoftheresearchdirectionsofthe"NewConceptCirculationInvariantandItsAutomaticDetectionTechnology"projectoftheNationalNaturalScienceFoundation
8、.Inthispaper
