程序切片獲取方法的研究及其在程序驗(yàn)證中的應(yīng)用.pdf

1、自M.Weiser提出程序切片的概念后，程序切片技術(shù)已應(yīng)用于程序調(diào)試、程序測(cè)試、程序的維護(hù)和程序的度量等多個(gè)領(lǐng)域。本課題將程序切片技術(shù)引入到程序驗(yàn)證領(lǐng)域：程序的公理化證明方法和模型檢測(cè)方法中。程序的公理化證明是應(yīng)用Hoare邏輯對(duì)程序進(jìn)行推理證明，其證明過(guò)程復(fù)雜。模型檢測(cè)自動(dòng)化的程度比較高，是用時(shí)序邏輯來(lái)表述的，存在狀態(tài)爆炸難題。本課題完成的主要工作有：
　　1、程序切片系統(tǒng)的構(gòu)建
　　程序切片的獲得需要提取源程序中的控制信

2、息和數(shù)據(jù)流信息，本課題通過(guò)正則表達(dá)式的構(gòu)建完成詞法分析器的構(gòu)造工作，通過(guò)LL(1)語(yǔ)法分析方法實(shí)現(xiàn)了語(yǔ)法分析器。通過(guò)詞法和語(yǔ)法的分析，提取出了程序切片所需的基本信息。
　　2、提出了反向控制流的程序切片算法
　　對(duì)M.Weiser提出的數(shù)據(jù)流方程切片算法以及K.J.Ottenstein和L.M.Ottenstein圖的可達(dá)性算法分析后提出了反向控制流的程序切片算法，降低了程序切片時(shí)的時(shí)間和空間的開銷。
　　3、將程序切