程序切片獲取方法的研究及其在程序驗證中的應用.pdf

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

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