基于約束的Prolog語(yǔ)義及其在Prolog程序測(cè)試、分析及驗(yàn)證中的應(yīng)用研究.pdf

1、以Prolog為代表的邏輯程序設(shè)計(jì)(LP)語(yǔ)言是一類重要的人工智能應(yīng)用語(yǔ)言。其主要特點(diǎn)是問(wèn)題描述和問(wèn)題求解過(guò)程的分離。如何利用LP語(yǔ)言開(kāi)發(fā)正確可靠的應(yīng)用軟件系統(tǒng)是邏輯程序設(shè)計(jì)研究的熱點(diǎn)之一。本文以基于約束的Prolog形式語(yǔ)義和抽象解釋理論為工具，對(duì)Prolog程序測(cè)試、調(diào)試、分析和驗(yàn)證過(guò)程中遇到的問(wèn)題進(jìn)行了探索和研究。課題得到了國(guó)家自然科學(xué)基金和廣西科學(xué)基金的資助。論文主要研究結(jié)果包括： 1)針對(duì)現(xiàn)有Prolog語(yǔ)義在描述與程

2、序點(diǎn)相關(guān)程序性質(zhì)上的不足，給出了一種攜帶路徑信息并允許cut操作的Prolog抽象語(yǔ)法，并基于此給出了一種Prolog操作語(yǔ)義、目標(biāo)獨(dú)立的標(biāo)號(hào)樹(shù)語(yǔ)義和D-標(biāo)號(hào)樹(shù)語(yǔ)義，證明了標(biāo)號(hào)樹(shù)語(yǔ)義和D-標(biāo)號(hào)樹(shù)語(yǔ)義相對(duì)于操作語(yǔ)義的正確性。 2)作為D-標(biāo)號(hào)樹(shù)語(yǔ)義的抽象，給出了一種獨(dú)立于目標(biāo)的Prolog路徑依賴部分解語(yǔ)義。由該語(yǔ)義可計(jì)算任意目標(biāo)的執(zhí)行過(guò)程中在每一個(gè)程序點(diǎn)獲得的部分解。利用現(xiàn)有的語(yǔ)義抽象技術(shù)該語(yǔ)義可以抽象為一個(gè)有限可計(jì)算的語(yǔ)義，從

3、而可進(jìn)行目標(biāo)獨(dú)立的Prolog程序分析。 3)把Prolog路徑依賴部分解語(yǔ)義用于基于抽象解釋的Prolog程序驗(yàn)證，給出了一種驗(yàn)證與Prolog程序點(diǎn)相關(guān)聯(lián)程序性質(zhì)的方法。本文例子表明了該驗(yàn)證方法的有效性。 4)給出了一種綜合的邏輯程序測(cè)試和調(diào)試框架，基于該框架的邏輯程序測(cè)試和調(diào)試算法可減少對(duì)調(diào)試過(guò)程不必要的調(diào)用，從而提高軟件開(kāi)發(fā)的效率。在一種基于約束的Prolog計(jì)算解語(yǔ)義(該語(yǔ)義可視為D-標(biāo)號(hào)樹(shù)語(yǔ)義的抽象)的基礎(chǔ)上

4、，給出了該框架的一個(gè)實(shí)例，說(shuō)明了該框架的應(yīng)用。 5)以Prolog程序控制流圖的隱式表示為基礎(chǔ)，給出了一種基于調(diào)用模式語(yǔ)義的Prolog程序測(cè)試用例生成方法。所使用的調(diào)用模式語(yǔ)義可視為D-標(biāo)號(hào)樹(shù)語(yǔ)義的另一抽象。與由于顯式控制流圖規(guī)模龐大而不得不采用不完整控制流圖的Prolog程序測(cè)試相比，隱式表示中包含完整的控制流信息，且允許測(cè)試人員通過(guò)適當(dāng)?shù)恼Z(yǔ)義抽象靈活地適應(yīng)測(cè)試的要求。 6)研究了調(diào)用模式語(yǔ)義在Prolog程序CPM