[發明專利]一種基于語法樹的程序正確性驗證方法

在審

• 申請號: 200810060942.3
• 申請日: 2008-04-08
• 公開（公告）號: CN101261602A
• 公開（公告）日: 2008-09-10
• 發明（設計）人: 吳卿;胡維華;謝紅標;周必水
• 申請（專利權）人: 杭州電子科技大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 杭州求是專利事務所有限公司
• 代理人: 張法高

技術領域

本發明屬于計算機應用技術領域，特別是涉及一種程序設計正確性驗證的方法。

背景技術

程序正確性驗證是IT技能測評自動化的一項重要內容，也是其中的一個理論、技術難點。程序的正確性，是指對于給定領域的所有的輸入，程序都能給出正確的輸出，程序都能給出正確的輸出。然而正如Dijkstra所指出：“我們可以通過測試發現程序中存在的錯誤，但無法證明不存在錯誤。”通常情況下，即使是一個非常簡單的程序，都可能具有無限多個可能的輸入。

目前，進行程序正確性驗證通常有兩種方案：第一種，完全拋棄檢查輸入-輸出的方法，通過形式語言理解來判斷程序的正確性；第二種方案則維持采用檢查輸入-輸出的方法，但不是檢查所有的可能輸入，而是檢查領域問題的各種“典型”輸入。限于形式語言理解研究的發展水平，第一種方案的研究、發展非常緩慢。國內外學者將研究的重點放在第二種方案上，也就是典型測試數據的自動生成，并提出了一些切實可的方法，如符號執行方法、迭代張弛法等，但這些方法的效率以及驗證的準確性不夠。

發明內容

本發明的目的在于針對現有技術的不足，提供一種基于語法樹的程序正確性驗證方法。

本發明解決其技術問題采用的技術方案如下：

1)采用XML的格式將源程序轉換為程序語法樹，具體方法是：

分析待驗證程序的語義信息，轉換成XML格式的語義表達，映射為一棵無序標簽樹。其中，程序名及程序中的各元素轉化為相應層次的父節點和子節點；程序中的操作符、操作數為葉子節點。使用一個虛擬根節點將所有節點進行組合。

2)對程序語法樹進行優化，具體方法是：

采用常量合并、同類語義合并、無用變量刪除以及復雜表達式拆分的方法對1)中的程序語法樹進行分析，排除語義的多樣性，使同一功能呈現同一的語法樹表現形式。

3)使用XPath語句對2)中的優化后的程序語法樹進行表達，每一條XPath語句都對應一個權重，具體方法是：

①對于XPath語句組中的每一條XPath語句依次檢驗，如果XPath語句在待驗證語法樹中查詢結果與在匹配樹中的查詢結果一致，則此XPath語句對應的權重值累加到作為結果的匹配度中；

②一組XPath語句查詢完成，生成匹配樹，將得到的匹配度作為最小匹配代價。

4)利用XPath路徑的匹配方法驗證源程序整體的正確性，具體方法是：

將匹配樹與每一待驗證樹進行比較。取匹配樹的每條路徑并在待驗證樹中查找對應路徑根節點。如果未找到該根節點，則完全不匹配，源程序整體錯誤，退出驗證。如果找到該根節點，則進入5)。

5)對待驗證樹中的單條路徑進行驗證，如果待驗證樹中的節點n是查詢樹的第k條路徑的根節點，并且與以節點n為根的子樹和匹配樹中的第k條路徑相匹配，則待驗證樹與匹配樹在其第k條路徑上匹配，即驗證第k條路徑所對應的源程序正確。

6)通過5)對待驗證樹中的全路徑進行驗證，如果部分路徑上匹配，則對應該路徑的源程序正確；如果所有路徑上匹配，則源程序整體正確。

本發明是一種基于語法樹的程序正確性驗證方法，其主要功能是通過該方法以程序的語法樹作為程序正確性的檢驗對象，運用無序標簽樹語義匹配算法，驗證目標程序的正確性。本方法實現程序的正確性自動驗證，為計算機程序自動測評提供了方法保障。

(1)語義形式化。程序語法樹是程序結構的樹狀表示，是形式化、規范化的程序語義表示，是程序設計者思想的形式化表示，比源程序具有更低的層次，能夠形象地抽象出程序結構，便于程序正確性的驗證；

(2)高效性。引入Xpath使得在匹配XML文檔結構樹時能夠準確地找到某一個節點元素。將XPath比作文件管理路徑，通過文件管理路徑，按照一定的規則查找到所需要的文件。同理，根據XPath所制定的規則，能夠快速找到XML結構文檔樹中的任何一個節點。每一條XPath語句都有一個返回結果，若查找到該節點則返回值為True，或節點的值；當查詢節點不存在時，返回結果為False。

具體實施方式

1方法中涉及到相關的定義及說明：