程序自動化調試的多謂詞開關方法.pdf

1、程序調試是軟件開發(fā)過程中最關鍵的環(huán)節(jié)之一，調試的開銷將直接影響到軟件的成本和軟件公司的收益。對于程序員來說，調試也是一個非常單調乏味的工作。因此，程序的自動化調試方法成為了計算機領域的熱點課題，得到不同領域眾多研究者的關注，繼而出現(xiàn)了各種各樣的自動化調試方法，如算法調試、切片技術、基于模型調試、基于概率調試、基于程序狀態(tài)調試、Delta調試等等。
　　 現(xiàn)有的大多數(shù)調試技術都是經(jīng)驗性的，即依靠專家經(jīng)驗和一些啟發(fā)式性質。為此，劉詠

2、梅教授分析了要基于第一原理為程序調試建立一個精確的理論基礎的重要性。本文研究的起點是張翔宇教授等人提出的一種程序調試的單謂詞開關方法，其主要思想是通過改變程序運行過程中的一個謂詞實例的取值使得原來錯誤的程序最終運行得到正確的結果，然后根據(jù)被開關的謂詞利用切片技術來確定診斷范圍。但很多情況下，只對單個謂詞實例進行開關并不能夠使程序得到正確的運行。針對單謂詞開關算法的局限性，本文提出有界調試的多謂詞開關算法(bounded debuggin

3、g via multiple predicate switchingalgorithm，BMPS)，通過在程序運行過程中開關多個謂詞實例來得到一個正確的運行，且在此運行中每個循環(huán)的執(zhí)行次數(shù)不超過一個給定的上界。BMPS算法可以通過一個可滿足性(satisfiability，SAT)求解器來實現(xiàn)。
　　 文中討論的程序錯誤主要為右端(righthandside，RHS)錯誤，即錯誤出現(xiàn)在控制謂詞或者賦值語句的右邊。對于只含條件控制

4、語句的程序，本文證明了BMPS算法對于RHS錯誤是準完備的，即真實錯誤的部分語句一定會被BMPS算法返回。對于含循環(huán)的程序，本文證明了當循環(huán)展開的次數(shù)足夠大時，BMPS算法對于RHS錯誤是準完備的。
　　 本文對所提BMPS算法進行了初步的實驗評估。本文深入分析了調試領域權威標準西門子標準中的TCAS程序，得出TCAS程序的41個錯誤版本中有39個版本是RHS錯誤。本文還對大量小型錯誤C程序進行了調試實驗，實驗結果表明BMPS能