程序自動化調(diào)試的多謂詞開關(guān)方法.pdf

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

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

3、g via multiple predicate switchingalgorithm，BMPS)，通過在程序運行過程中開關(guān)多個謂詞實例來得到一個正確的運行，且在此運行中每個循環(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算法進行了初步的實驗評估。本文深入分析了調(diào)試領(lǐng)域權(quán)威標準西門子標準中的TCAS程序，得出TCAS程序的41個錯誤版本中有39個版本是RHS錯誤。本文還對大量小型錯誤C程序進行了調(diào)試實驗，實驗結(jié)果表明BMPS能