發(fā)布時(shí)間：2020-07-11 09:58

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

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

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

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

【參考文獻(xiàn)】

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

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

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

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

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

本文編號(hào)：2750253