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

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

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

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

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