【摘要】：循環(huán)程序的終止性分析是程序驗證的重要組成部分。確保循環(huán)程序的終止是循環(huán)程序完全正確的必要條件。目前,用來證明程序終止性的主流方法是通過合成秩函數(shù)的方法來證明。秩函數(shù)是一個關(guān)于循環(huán)變量的函數(shù),其值域是一個良基集,它的函數(shù)值隨著循環(huán)體的執(zhí)行持續(xù)減小。本文給出了如何通過合成復雜秩函數(shù)的方法來證明循環(huán)程序的終止性,并介紹了循環(huán)程序終止性自動驗證工具TermChecker。目前合成秩函數(shù)的主要方法是通過設定秩函數(shù)模板,然后求解模板參數(shù)來完成的。傳統(tǒng)定義的秩函數(shù)要求循環(huán)的每次迭代都使得函數(shù)值都減小,這種較強的約束往往使得模板參數(shù)無解,這嚴重限制了通過合成秩函數(shù)來證明循環(huán)程序的終止。因此,在本文中,首先將傳統(tǒng)秩函數(shù)的概念進行了推廣,提出了k階秩函數(shù)的概念,并通過合成k階秩函數(shù)來證明單分支線性賦值循環(huán)程序的終止性。傳統(tǒng)的秩函數(shù)只是k階秩函數(shù)的一種特殊情況。針對多分支循環(huán)程序的終止性的證明,傳統(tǒng)的方法是通過合成字典序秩函數(shù)或者全局秩函數(shù)來證明的。但是,多分支循環(huán)程序存在字典序秩函數(shù)或者全局秩函數(shù)只是對應多分支循環(huán)程序終止的充分條件,而非必要條件。因此,為了進一步擴大秩函數(shù)的適用范圍,本文提出了一個多分支線性賦值循環(huán)程序終止的充分標準。該標準通過合成多分支線性賦值循環(huán)程序的局部秩函數(shù)來證明對應循環(huán)程序的終止性。實驗結(jié)果表明針對某些終止的多分支線性賦值循環(huán)程序,不能通過合成字典序秩函數(shù)或者全局秩函數(shù)來證明它的終止,但是可以通過合成局部秩函數(shù)來證明。為了實現(xiàn)循環(huán)程序終止性的自動驗證,開發(fā)了工具TermChecker。該工具可以實現(xiàn)C語言編寫的循環(huán)程序片段的終止性自動分析工作。軟件首先對輸入的循環(huán)程序進行詞法分析、語法分析,然后提取出循環(huán)信息并將其傳給服務器端。服務器端的循環(huán)程序終止性分析算法使用符號計算軟件Maple編寫,該算法供服務器端的C程序調(diào)用對循環(huán)信息進行分析,然后將分析結(jié)果返回給客戶端。最后客戶端顯示分析結(jié)果。
【學位授予單位】：重慶郵電大學
【學位級別】：碩士
【學位授予年份】：2018
【分類號】：TP312.1;TP311.53
【圖文】：

在符號計算領域發(fā)展多年，有許多高效的函數(shù)可以供調(diào)用，這將極大的方便我們的計算推導過程。Mathematica 本來兼具符號計算和數(shù)值計算，但是其符號計算的能力和函數(shù)庫的豐富程度還有所欠缺，因此我們不選用該計算軟件。RegularChains 是Maple 的一個包，可以在 Maple 下加載調(diào)用。其中包含了許多子包和函數(shù)，可用于求解多項式等式、不等式和符號不等式系統(tǒng)。其中的命令 QuantifierElimination 可用于量詞消去。本章我們利用 RegularChains 中的函數(shù)進行秩函數(shù)的合成計算。下面，通過一個實例來介紹 RegularChains 的使用。對于如下所示的量詞公式 x , y ( x 1 x 9 y x 0 y 0 ax by c 0)表 示 對 于 任 意 的 x,y, 當x 1 x 9 y x 0 y 0時，可以推出 ax by c 0，其中 a，b，c 是參數(shù)。為方便討論，我們令 f ax by c，接下來，我們通過 RegularChains 來演示如何求出一組合適的 a，b，c 來滿足上述的量詞公式。

重慶郵電大學碩士學位論文 第 2 章 單分支線性賦值循環(huán)程序的終止性分析如圖 2.1 所示，首先需要指定 RegularChains 的路徑參數(shù) libname，這是因為目前 Maple 中自帶的 RegularChains 包中還沒有將最新的量詞消去函數(shù)QuantifierElimination 包含進去，因此本文中計算所需的 RegularChains 包需要到http://www.regularchains.org/downloads.html 去下載最新版本，然后將其放在 E 盤下面，通過 libname 參數(shù)來指定加載。然后我們依次加載 RegularChains 和SemiAlgebraicSetTools.

圖 2.2 使用 QuantifierElimination 命令進行量詞消去首先輸入量詞公式 x , y ( x 1 x 9 y x 0 y 0 ax by c 0)并命名為 p1，然后使用 QuantifierElimination 命令消去 x,y 得到 a，b，c 的約束條件，并將該約束條件命名為 t1.接下來需要判斷是否存在 a，b，c 滿足約束 t1，將該存在量詞公式命名為 p2，再一次調(diào)用 QuantifierElimination 進行判斷，得到 true 即表明約束t1 是有解的。

【參考文獻】

相關(guān)期刊論文 前4條

1 李軼;李傳璨;吳文淵;;多分支單變量循環(huán)程序的終止性分析[J];軟件學報;2015年02期

2 李軼;吳文淵;馮勇;;有界閉域上的線性賦值循環(huán)終止性分析[J];軟件學報;2014年06期

3 李軼;;線性循環(huán)程序的終止性判定[J];系統(tǒng)科學與數(shù)學;2013年05期

4 李軼;;非線性循環(huán)的終止性分析[J];軟件學報;2012年05期

本文編號：2750253